1  /-
  2  Copyright (c) 2018 Chris Hughes. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Chris Hughes, Abhimanyu Pallavi Sudhir
  5  -/
  6  import algebra.archimedean algebra.geom_sum
src         └─────────────────┘ └──────────────┘
  7  import data.nat.choose data.complex.basic
src         └─────────────┘ └────────────────┘
  8  import tactic.linarith
src         └─────────────┘
  9  
 10  local notation `abs'` := _root_.abs
id                            └────────┘
src                           └────────┘
typ                           └────────┘
 11  open is_absolute_value
 12  open_locale classical
 13  
 14  section
 15  open real is_absolute_value finset
 16  
 17  lemma forall_ge_le_of_forall_le_succ {α : Type*} [preorder α] (f : ℕ → α) {m : ℕ}
id                                                     └──────┘                  
src                                                    └──────┘                    
typ                                                    └──────┘                  
 18    (h : ∀ n ≥ m, f n.succ ≤ f n) : ∀ {l}, ∀ k ≥ m, k ≤ l → f l ≤ f k :=
id                  └───┘                             
src                    └───┘                                    
typ                 └───┘                             
 19  begin
st   └─────
 20    assume l k hkm hkl,
src    └────────────────┘
typ    └────────────────┘
doc    └────────────────┘
txt    └────────────────┘
par    └────────────────┘
pid    └────────────────┘
st   ───────────────────┘└─
 21    generalize hp : l - k = p,
id                       
src    └──────────────┘   
typ    └──────────────┘ 
doc    └──────────────┘    
txt    └──────────────┘    
par    └──────────────┘    
pid              └─┘└┘    
st   ──────────────────────────┘└─
 22    have : l = k + p := add_comm p k ▸ (nat.sub_eq_iff_eq_add hkl).1 hp,
id                     └──────┘     └───────────────────┘ └─┘    └┘
src    └─────┘    └──┘└──────┘   └───────────────────┘   └──┘
typ    └─────┘ └──┘└──────┘ └───────────────────┘└─┘└──┘└┘
doc    └─────┘     └──┘                                    └──┘
txt    └─────┘     └──┘                                    └──┘
par    └─────┘     └──┘                                    └──┘
pid    └───┘└┘     └──┘                                    └──┘
st   ────────────────────────────────────────────────────────────────────┘└─
 23    subst this,
id           └──┘
src    └────┘
typ    └────┘└──┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ───────────┘└─
 24    clear hkl hp,
src    └──────────┘
typ    └──────────┘
doc    └──────────┘
txt    └──────────┘
par    └──────────┘
pid         └─────┘
st   ─────────────┘└─
 25    induction p with p ih,
id               
src    └────────┘ └────────┘
typ    └────────┘└────────┘
doc    └────────┘ └────────┘
txt    └────────┘ └────────┘
par    └────────┘ └────────┘
pid              └───────┘
st   ──────────────────────┘└─
 26    { simp },
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ───┘└───┘└┘
 27    { exact le_trans (h _ (le_trans hkm (nat.le_add_right _ _))) ih }
id                           └──────┘ └─┘  └──────────────┘        └┘
src      └────┘          └─┘ └──────┘    └──────────────┘└──────┘  
typ      └────┘         └─┘ └──────┘└─┘ └──────────────┘└──────┘└┘
doc      └────┘          └─┘                             └──────┘  
txt      └────┘          └─┘                             └──────┘  
par      └────┘          └─┘                             └──────┘  
pid                     └─┘                             └──────┘  
st   ─────────────────────────────────────────────────────────────────┘└─
 28  end
st   ──┘
 29  
 30  variables {α : Type*} {β : Type*} [ring β]
id                                    └──┘
src                                     └──┘
typ                                   └──┘
 31    [discrete_linear_ordered_field α] [archimedean α] {abv : β → α} [is_absolute_value abv]
id      └───────────────────────────┘     └─────────┘                   └───────────────┘
src     └───────────────────────────┘     └─────────┘                   └───────────────┘
typ     └───────────────────────────┘     └─────────┘                   └───────────────┘
doc                                                                     └───────────────┘
 32  
 33  lemma is_cau_of_decreasing_bounded (f : ℕ → α) {a : α} {m : ℕ} (ham : ∀ n ≥ m, abs (f n) ≤ a)
id                                                                            └─┘      
src                                                                               └─┘       
typ                                                                           └─┘      
 34    (hnm : ∀ n ≥ m, f n.succ ≤ f n) : is_cau_seq abs f :=
id                    └───┘       └────────┘ └─┘ 
src                       └───┘         └────────┘ └─┘
typ                   └───┘       └────────┘ └─┘ 
doc                                      └────────┘
 35  λ ε ε0,
id      └┘
typ     └┘
 36  let ⟨k, hk⟩ := archimedean.arch a ε0 in
id   └─┘           └──────────────┘  └┘
src                 └──────────────┘
typ  └─┘           └──────────────┘  └┘
 37  have h : ∃ l, ∀ n ≥ m, a - add_monoid.smul l ε < f n :=
id                       └─────────────┘     
src                          └─────────────┘     
typ                      └─────────────┘     
 38    ⟨k + k + 1, λ n hnm, lt_of_lt_of_le
id                  └─┘  └────────────┘
src                       └────────────┘
typ                 └─┘  └────────────┘
 39      (show a - add_monoid.smul (k + (k + 1)) ε < -abs (f n),
id               └─────────────┘               └─┘   
src               └─────────────┘                └─┘
typ              └─────────────┘               └─┘   
 40        from lt_neg.1 $ lt_of_le_of_lt (ham n hnm) (begin
id              └────┘    └────────────┘  └─┘  └─┘
src             └────┘    └────────────┘
typ             └────┘    └────────────┘  └─┘  └─┘
st                                                     └─────
 41          rw [neg_sub, lt_sub_iff_add_lt, add_monoid.add_smul],
id               └─────┘  └───────────────┘  └─────────────────┘
src          └──┘└─────┘└┘└───────────────┘└┘└─────────────────┘
typ          └──┘└─────┘└┘└───────────────┘└┘└─────────────────┘
doc          └──┘       └┘                 └┘                   
txt          └──┘       └┘                 └┘                   
par          └──┘       └┘                 └┘                   
pid            └┘       └┘                 └┘                   
st   ──────────────────┘└─────────────────┘└───────────────────┘└──
 42          exact add_lt_add_of_le_of_lt hk (lt_of_le_of_lt hk
id                 └────────────────────┘     └────────────┘ └┘
src          └────┘└────────────────────┘   └────────────┘  
typ          └────┘└────────────────────┘   └────────────┘└┘
doc          └────┘                                         
txt          └────┘                                         
par          └────┘                                         
pid                                                        
st   ───────────────────────────────────────────────────────────
 43            (lt_add_of_pos_left _ ε0)),
id              └────────────────┘   └┘
src  ─────────┘ └────────────────┘└─┘  └┘
typ  ─────────┘ └────────────────┘└─┘└┘└┘
doc  ─────────┘                   └─┘  └┘
txt  ─────────┘                   └─┘  └┘
par  ─────────┘                   └─┘  └┘
pid  ─────────┘                   └─┘  └┘
st   ───────────────────────────────────┘└─
 44        end))
st   ────────┘
 45      (neg_le.2 $ (abs_neg (f n)) ▸ le_abs_self _)⟩,
id        └────┘     └─────┘       └─────────┘
src       └────┘     └─────┘         └─────────┘
typ       └────┘     └─────┘       └─────────┘
 46  let l := nat.find h in
id           └──────┘ 
src           └──────┘
typ          └──────┘ 
 47  have hl : ∀ (n : ℕ), n ≥ m → f n > a - add_monoid.smul l ε := nat.find_spec h,
id                                 └─────────────┘      └───────────┘ 
src                                     └─────────────┘        └───────────┘
typ                                └─────────────┘      └───────────┘ 
 48  have hl0 : l ≠ 0 := λ hl0, not_lt_of_ge (ham m (le_refl _))
id                       └─┘  └──────────┘  └─┘   └─────┘
src                            └──────────┘         └─────┘
typ                      └─┘  └──────────┘  └─┘   └─────┘
 49    (lt_of_lt_of_le (by have := hl m (le_refl m); simpa [hl0] using this) (le_abs_self (f m))),
id      └────────────┘             └┘    └─────┘           └─┘        └──┘   └─────────┘   
src     └────────────┘     └──────┘    └─────┘   └─────┘   └──────┘       └─────────┘
typ     └────────────┘     └──────┘└┘  └─────┘  └─────┘└─┘└──────┘└──┘   └─────────┘   
doc                        └──────┘              └─────┘   └──────┘
txt                        └──────┘              └─────┘   └──────┘
par                        └──────┘              └─────┘   └──────┘
pid                        └───┘└─┘                      └────┘
st                        └───────────────────────────────────────────────┘
 50  begin
st   └─────
 51    cases classical.not_forall.1
id           └──────────────────┘
src    └────┘└──────────────────┘└──
typ    └────┘└──────────────────┘└──
doc    └────┘                    └──
txt    └────┘                    └──
par    └────┘                    └──
pid                             └──
st   ───────────────────────────────
 52      (nat.find_min h (nat.pred_lt hl0)) with i hi,
id        └──────────┘   └─────────┘ └─┘
src  ───┘ └──────────┘  └─────────┘   └──────────┘
typ  ───┘ └──────────┘ └─────────┘└─┘└──────────┘
doc  ───┘                             └──────────┘
txt  ───┘                             └──────────┘
par  ───┘                             └──────────┘
pid  ───┘                             └┘└────────┘
st   ───────────────────────────────────────────────┘└─
 53    rw [not_imp, not_lt] at hi,
id         └─────┘  └────┘
src    └──┘└─────┘└┘└────┘└─────┘
typ    └──┘└─────┘└┘└────┘└─────┘
doc    └──┘       └┘      └─────┘
txt    └──┘       └┘      └─────┘
par    └──┘       └┘      └─────┘
pid      └┘       └┘      └────┘
st   ────────────┘└──────┘└────┘└─
 54    existsi i,
id             
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid           
st   ──────────┘└─
 55    assume j hj,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid    └─────────┘
st   ────────────┘└─
 56    have hfij : f j ≤ f i := forall_ge_le_of_forall_le_succ f hnm _ hi.1 hj,
id                          └────────────────────────────┘  └─┘   └┘   └┘
src    └──────────┘    └──┘└────────────────────────────┘    └─┘  └─┘
typ    └──────────┘ └──┘└────────────────────────────┘└─┘└─┘└┘└─┘└┘
doc    └──────────┘     └──┘                                  └─┘  └─┘
txt    └──────────┘     └──┘                                  └─┘  └─┘
par    └──────────┘     └──┘                                  └─┘  └─┘
pid    └───────┘└─┘     └──┘                                  └─┘  └─┘
st   ────────────────────────────────────────────────────────────────────────┘└─
 57    rw [abs_of_nonpos (sub_nonpos.2 hfij), neg_sub, sub_lt_iff_lt_add'],
id         └───────────┘  └────────┘   └──┘   └─────┘  └────────────────┘
src    └──┘└───────────┘ └────────┘└─┘    └─┘└─────┘└┘└────────────────┘
typ    └──┘└───────────┘ └────────┘└─┘└──┘└─┘└─────┘└┘└────────────────┘
doc    └──┘                        └─┘    └─┘       └┘                  
txt    └──┘                        └─┘    └─┘       └┘                  
par    └──┘                        └─┘    └─┘       └┘                  
pid      └┘                        └─┘    └─┘       └┘                  
st   ──────────────────────────────────────┘└───────┘└──────────────────┘└──
 58    exact calc f i ≤ a - add_monoid.smul (nat.pred l) ε : hi.2
id                        └─────────────┘  └──────┘   
src    └────┘         └─────────────┘ └──────┘ └┘ └─┘  └──
typ    └────┘       └─────────────┘ └──────┘└┘└─┘  └──
doc    └────┘                                  └┘ └─┘  └──
txt    └────┘                                  └┘ └─┘  └──
par    └────┘                                  └┘ └─┘  └──
pid                                           └┘ └─┘  └──
st   ─────────────────────────────────────────────────────────────
 59      ... = a - add_monoid.smul l ε + ε :
id                                    
src  ───────┘                    └──
typ  ───────┘                    └──
doc  ───────┘                      └──
txt  ───────┘                      └──
par  ───────┘                      └──
pid  ───────┘                      └──
st   ────────────────────────────────────────
 60        by conv {to_rhs, rw [← nat.succ_pred_eq_of_pos (nat.pos_of_ne_zero hl0), succ_smul',
id                                └─────────────────────┘  └────────────────┘ └─┘   └────────┘
src  ─────┘  └────┘└────┘└┘└────┘└─────────────────────┘ └────────────────┘   └─┘└────────┘└─
typ  ─────┘  └────┘└────┘└┘└────┘└─────────────────────┘ └────────────────┘└─┘└─┘└────────┘└─
doc  ─────┘  
txt  ─────┘  └────┘└────┘└┘└────┘                                             └─┘          └─
par  ─────┘  └────┘└────┘└┘└────┘                                             └─┘          └─
pid  ─────┘  └───────────────────┘                                             └─┘          └─
st   ───────┘└─────┘└────┘└──────────────────────────────────────────────────────┘└──────────┘└─
 61          sub_add, add_sub_cancel] }
id           └─────┘  └────────────┘
src  ───────┘└─────┘└┘└────────────┘└┘└─
typ  ───────┘└─────┘└┘└────────────┘└┘└─
txt  ───────┘       └┘              └┘└─
par  ───────┘       └┘              └┘└─
pid  ───────┘       └┘              └───
st   ──────────────┘└──────────────┘ 
 62      ... < f j + ε : add_lt_add_right (hl j (le_trans hi.1 hj)) _
id                      └──────────────┘  └┘   └──────┘ └┘   └┘
src  ───┘└──┘     └─┘└──────────────┘     └──────┘  └─┘  └───┘
typ  ───┘└──┘    └─┘└──────────────┘ └┘ └──────┘└┘└─┘└┘└───┘
doc      └──┘     └─┘                               └─┘  └───┘
txt  ───┘└──┘     └─┘                               └─┘  └───┘
par  ───┘└──┘     └─┘                               └─┘  └───┘
pid  ───────┘     └─┘                               └─┘  └──┘
st   ───┘└───────────────────────────────────────────────────────────┘
 63  end
st   └─┘
 64  
 65  lemma is_cau_of_mono_bounded (f : ℕ → α) {a : α} {m : ℕ} (ham : ∀ n ≥ m, abs (f n) ≤ a)
id                                                                      └─┘      
src                                                                         └─┘       
typ                                                                     └─┘      
 66    (hnm : ∀ n ≥ m, f n ≤ f n.succ) : is_cau_seq abs f :=
id                       └───┘    └────────┘ └─┘ 
src                            └───┘    └────────┘ └─┘
typ                      └───┘    └────────┘ └─┘ 
doc                                      └────────┘
 67  begin
st   └─────
 68    refine @eq.rec_on (ℕ → α) _ (is_cau_seq abs) _ _
id             └───────┘            └────────┘
src    └─────┘ └───────┘    └──┘ └────────┘   └─────
typ    └─────┘ └───────┘    └──┘ └────────┘   └─────
doc    └─────┘              └──┘ └────────┘   └─────
txt    └─────┘              └──┘              └─────
par    └─────┘              └──┘              └─────
pid                        └──┘              └─────
st   ───────────────────────────────────────────────────
 69      (-⟨_, @is_cau_of_decreasing_bounded _ _ _ (λ n, -f n) a m (by simpa) (by simpa)⟩ : cau_seq α abs).2,
id             └──────────────────────────┘                                             └─────┘  └─┘
src  ───┘  └─┘ └──────────────────────────┘└─────┘  └──┘   └┘     └───┘└┘   └───┘└───┘└─────┘ └─┘└─┘
typ  ───┘  └─┘ └──────────────────────────┘└─────┘  └──┘  └┘   └───┘└┘   └───┘└───┘└─────┘└─┘└─┘
doc  ───┘   └─┘                             └─────┘  └──┘   └┘     └───┘└┘   └───┘└───┘           └─┘
txt  ───┘   └─┘                             └─────┘  └──┘   └┘     └───┘└┘   └───┘└───┘           └─┘
par  ───┘   └─┘                             └─────┘  └──┘   └┘     └───┘└┘   └───┘└───┘           └─┘
pid  ───┘   └─┘                             └─────┘  └──┘   └┘     └──────┘   └─────────┘           └┘
st   ────────────────────────────────────────────────────────────────┘└────┘└───┘└────┘└───────────────────┘└─
 70    ext,
src    └─┘
typ    └─┘
doc    └─┘
txt    └─┘
par    └─┘
st   ────┘└─
 71    exact neg_neg _
id           └─────┘
src    └────┘└─────┘└─┘
typ    └────┘└─────┘└─┘
doc    └────┘       └─┘
txt    └────┘       └─┘
par    └────┘       └─┘
pid                └┘
st   ─────────────────┘
 72  end
st   └─┘
 73  
 74  lemma is_cau_series_of_abv_le_cau  {f : ℕ → β} {g : ℕ → α}  (n : ℕ) : (∀ m, n ≤ m → abv (f m) ≤ g m) →
id                                                                              └─┘       
src                                                                                            
typ                                                                             └─┘       
 75    is_cau_seq abs (λ n, (range n).sum g) → is_cau_seq abv (λ n, (range n).sum f) :=
id     └────────┘ └─┘       └───┘  └─┘      └────────┘ └─┘       └───┘  └─┘  
src    └────────┘ └─┘       └───┘   └─┘       └────────┘            └───┘   └─┘
typ    └────────┘ └─┘       └───┘  └─┘      └────────┘ └─┘       └───┘  └─┘  
doc    └────────┘            └───┘             └────────┘            └───┘
 76  begin
st   └─────
 77    assume hm hg ε ε0,
src    └───────────────┘
typ    └───────────────┘
doc    └───────────────┘
txt    └───────────────┘
par    └───────────────┘
pid    └───────────────┘
st   ──────────────────┘└─
 78    cases hg (ε / 2) (div_pos ε0 (by norm_num)) with i hi,
id           └┘        └─────┘ └┘
src    └────┘    └──┘ └─────┘     └──────┘└──────────┘
typ    └────┘└┘ └──┘ └─────┘└┘   └──────┘└──────────┘
doc    └────┘     └──┘             └──────┘└──────────┘
txt    └────┘     └──┘             └──────┘└──────────┘
par    └────┘     └──┘             └──────┘└──────────┘
pid              └──┘             └─────────┘└────────┘
st   ─────────────────────────────────┘└───────┘└──────────┘└─
 79    existsi max n i,
id             └─┘  
src    └──────┘└─┘ 
typ    └──────┘└─┘
doc    └──────┘    
txt    └──────┘    
par    └──────┘    
pid               
st   ────────────────┘└─
 80    assume j ji,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid    └─────────┘
st   ────────────┘└─
 81    have hi₁ := hi j (le_trans (le_max_right n i) ji),
id                 └┘   └──────┘  └──────────┘    └┘
src    └──────────┘    └──────┘ └──────────┘  └┘  
typ    └──────────┘└┘ └──────┘ └──────────┘└┘└┘
doc    └──────────┘                           └┘  
txt    └──────────┘                           └┘  
par    └──────────┘                           └┘  
pid    └──────┘└─┘                           └┘  
st   ──────────────────────────────────────────────────┘└─
 82    have hi₂ := hi (max n i) (le_max_right n i),
id                 └┘  └─┘       └──────────┘  
src    └──────────┘   └─┘  └┘ └──────────┘  
typ    └──────────┘└┘ └─┘  └┘ └──────────┘
doc    └──────────┘        └┘               
txt    └──────────┘        └┘               
par    └──────────┘        └┘               
pid    └──────┘└─┘        └┘               
st   ────────────────────────────────────────────┘└─
 83    have sub_le := abs_sub_le ((range j).sum g) ((range i).sum g) ((range (max n i)).sum g),
id                    └────────┘                                      └───┘  └─┘         
src    └─────────────┘└────────┘        └────┘ └┘        └────┘ └┘  └───┘ └─┘  └─────┘ 
typ    └─────────────┘└────────┘       └────┘ └┘        └────┘ └┘  └───┘ └─┘└─────┘
doc    └─────────────┘                  └────┘ └┘        └────┘ └┘  └───┘      └─────┘ 
txt    └─────────────┘                  └────┘ └┘        └────┘ └┘             └─────┘ 
par    └─────────────┘                  └────┘ └┘        └────┘ └┘             └─────┘ 
pid    └─────────┘└─┘                  └────┘ └┘        └────┘ └┘             └─────┘ 
st   ────────────────────────────────────────────────────────────────────────────────────────┘└─
 84    have := add_lt_add hi₁ hi₂,
id             └────────┘ └─┘ └─┘
src    └──────┘└────────┘   
typ    └──────┘└────────┘└─┘└─┘
doc    └──────┘             
txt    └──────┘             
par    └──────┘             
pid    └───┘└─┘             
st   ───────────────────────────┘└─
 85    rw [abs_sub ((range (max n i)).sum g), add_halves ε] at this,
id         └─────┘   └───┘  └─┘            └────────┘ 
src    └──┘└─────┘  └───┘ └─┘  └─────┘ └─┘└────────┘ └───────┘
typ    └──┘└─────┘  └───┘ └─┘└─────┘└─┘└────────┘└───────┘
doc    └──┘         └───┘      └─────┘ └─┘           └───────┘
txt    └──┘                    └─────┘ └─┘           └───────┘
par    └──┘                    └─────┘ └─┘           └───────┘
pid      └┘                    └─────┘ └─┘           └──────┘
st   ──────────────────────────────────────┘└────────────┘└──────┘└─
 86    refine lt_of_le_of_lt (le_trans (le_trans _ (le_abs_self _)) sub_le) this,
id            └────────────┘            └──────┘    └─────────┘     └────┘  └──┘
src    └─────┘└────────────┘          └──────┘└─┘ └─────────┘└───┘└────┘└┘
typ    └─────┘└────────────┘          └──────┘└─┘ └─────────┘└───┘└────┘└┘└──┘
doc    └─────┘                                └─┘            └───┘      └┘
txt    └─────┘                                └─┘            └───┘      └┘
par    └─────┘                                └─┘            └───┘      └┘
pid                                          └─┘            └───┘      └┘
st   ──────────────────────────────────────────────────────────────────────────┘└─
 87    generalize hk : j - max n i = k,
id                       └─┘  
src    └──────────────┘ └─┘   
typ    └──────────────┘└─┘ 
doc    └──────────────┘        
txt    └──────────────┘        
par    └──────────────┘        
pid              └─┘└┘        
st   ────────────────────────────────┘└─
 88    clear this hi₂ hi₁ hi ε0 ε hg sub_le,
src    └──────────────────────────────────┘
typ    └──────────────────────────────────┘
doc    └──────────────────────────────────┘
txt    └──────────────────────────────────┘
par    └──────────────────────────────────┘
pid         └─────────────────────────────┘
st   ─────────────────────────────────────┘└─
 89    rw nat.sub_eq_iff_eq_add ji at hk,
id        └───────────────────┘ └┘
src    └─┘└───────────────────┘  └────┘
typ    └─┘└───────────────────┘└┘└────┘
doc    └─┘                       └────┘
txt    └─┘                       └────┘
par    └─┘                       └────┘
pid                             └────┘
st   ──────────────────────────────────┘└─
 90    rw hk,
id        └┘
src    └─┘
typ    └─┘└┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ──────┘└─
 91    clear hk ji j,
src    └───────────┘
typ    └───────────┘
doc    └───────────┘
txt    └───────────┘
par    └───────────┘
pid         └──────┘
st   ──────────────┘└─
 92    induction k with k' hi,
id               
src    └────────┘ └─────────┘
typ    └────────┘└─────────┘
doc    └────────┘ └─────────┘
txt    └────────┘ └─────────┘
par    └────────┘ └─────────┘
pid              └────────┘
st   ───────────────────────┘└─
 93    { simp [abv_zero abv] },
id             └──────┘ └─┘
src      └────┘└──────┘   └┘
typ      └────┘└──────┘└─┘└┘
doc      └────┘           └┘
txt      └────┘           └┘
par      └────┘           └┘
pid                     
st   ───┘└──────────────────┘└┘
 94    { dsimp at *,
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid           └──┘
st   ─────────────┘└─
 95      rw [nat.succ_add, sum_range_succ, sum_range_succ, add_assoc, add_assoc],
id           └──────────┘  └────────────┘  └────────────┘  └───────┘  └───────┘
src      └──┘└──────────┘└┘└────────────┘└┘└────────────┘└┘└───────┘└┘└───────┘
typ      └──┘└──────────┘└┘└────────────┘└┘└────────────┘└┘└───────┘└┘└───────┘
doc      └──┘            └┘              └┘              └┘         └┘         
txt      └──┘            └┘              └┘              └┘         └┘         
par      └──┘            └┘              └┘              └┘         └┘         
pid        └┘            └┘              └┘              └┘         └┘         
st   ───────────────────┘└──────────────┘└──────────────┘└─────────┘└─────────┘└──
 96      refine le_trans (abv_add _ _ _) _,
id              └──────┘  └─────┘
src      └─────┘└──────┘ └─────┘└───────┘
typ      └─────┘└──────┘ └─────┘└───────┘
doc      └─────┘                └───────┘
txt      └─────┘                └───────┘
par      └─────┘                └───────┘
pid                            └───────┘
st   ────────────────────────────────────┘└─
 97      exact add_le_add (hm _ (le_add_of_nonneg_of_le (nat.zero_le _) (le_max_left _ _))) hi },
id             └────────┘  └┘    └────────────────────┘  └─────────┘     └─────────┘        └┘
src      └────┘└────────┘   └─┘ └────────────────────┘ └─────────┘└──┘ └─────────┘└──────┘  
typ      └────┘└────────┘ └┘└─┘ └────────────────────┘ └─────────┘└──┘ └─────────┘└──────┘└┘
doc      └────┘             └─┘                                   └──┘            └──────┘  
txt      └────┘             └─┘                                   └──┘            └──────┘  
par      └────┘             └─┘                                   └──┘            └──────┘  
pid                        └─┘                                   └──┘            └──────┘  
st   ─────────────────────────────────────────────────────────────────────────────────────────┘└──
 98  end
st   ──┘
 99  
100  lemma is_cau_series_of_abv_cau {f : ℕ → β} : is_cau_seq abs (λ m, (range m).sum (λ n, abv (f n))) →
id                                              └────────┘ └─┘       └───┘  └─┘       └─┘   
src                                              └────────┘ └─┘        └───┘   └─┘
typ                                             └────────┘ └─┘       └───┘  └─┘       └─┘   
doc                                               └────────┘            └───┘
101    is_cau_seq abv (λ m, (range m).sum f) :=
id     └────────┘ └─┘       └───┘  └─┘  
src    └────────┘            └───┘   └─┘
typ    └────────┘ └─┘       └───┘  └─┘  
doc    └────────┘            └───┘
102  is_cau_series_of_abv_le_cau 0 (λ n h, le_refl _)
id   └─────────────────────────┘         └─────┘
src  └─────────────────────────┘           └─────┘
typ  └─────────────────────────┘         └─────┘
103  
104  lemma is_cau_geo_series {β : Type*} [field β] {abv : β → α} [is_absolute_value abv]
id                                        └───┘                └───────────────┘ └─┘
src                                       └───┘                   └───────────────┘
typ                                       └───┘                └───────────────┘ └─┘
doc                                                               └───────────────┘
105     (x : β) (hx1 : abv x < 1) : is_cau_seq abv (λ n, (range n).sum (λ m, x ^ m)) :=
id                    └─┘        └────────┘ └─┘       └───┘  └─┘         
src                                └────────┘            └───┘   └─┘          
typ                   └─┘        └────────┘ └─┘       └───┘  └─┘         
doc                                 └────────┘            └───┘
st                  
106  have hx1' : abv x ≠ 1 := λ h, by simpa [h, lt_irrefl] using hx1,
id               └─┘                        └───────┘        └─┘
src                                  └─────┘ └┘└───────┘└──────┘
typ              └─┘               └─────┘└┘└───────┘└──────┘└─┘
doc                                   └─────┘ └┘         └──────┘
txt                                   └─────┘ └┘         └──────┘
par                                   └─────┘ └┘         └──────┘
pid                                         └┘         └────┘
st                                   └─────────────────────────────┘
107  is_cau_series_of_abv_cau
id   └──────────────────────┘
src  └──────────────────────┘
typ  └──────────────────────┘
108  begin
st   └─────
109    simp only [abv_pow abv] {eta := ff},
id                └─────┘ └─┘          └┘
src    └─────────┘└─────┘   └┘ └─────┘└┘
typ    └─────────┘└─────┘└─┘└┘ └─────┘└┘
doc    └─────────┘          └┘ └─────┘  
txt    └─────────┘          └┘ └─────┘  
par    └─────────┘          └┘ └─────┘  
pid        └──┘└┘           └─────┘  
st   ────────────────────────────────────┘└─
110    have : (λ (m : ℕ), (range m).sum (λ n, (abv x) ^ n)) =
id                         └───┘                           
src    └─────┘  └────┘ └─┘ └───┘ └────┘  └──┘     └┘ └─┘
typ    └─────┘  └────┘ └─┘ └───┘ └────┘  └──┘     └┘ └─┘
doc    └─────┘  └────┘ └─┘ └───┘ └────┘  └──┘     └┘  └─┘ 
txt    └─────┘  └────┘ └─┘       └────┘  └──┘     └┘  └─┘ 
par    └─────┘  └────┘ └─┘       └────┘  └──┘     └┘  └─┘ 
pid    └───┘└┘  └────┘ └─┘       └────┘  └──┘     └┘  └─┘ 
st   ─────────────────────────────────────────────────────────
111     λ m, geom_series (abv x) m := rfl,
id           └─────────┘  └─┘        └─┘
src  ──┘ └──┘└─────────┘     └┘ └──┘└─┘
typ  ──┘ └──┘└─────────┘ └─┘└┘ └──┘└─┘
doc  ──┘ └──┘└─────────┘     └┘ └──┘
txt  ──┘ └──┘                └┘ └──┘
par  ──┘ └──┘                └┘ └──┘
pid  ──┘ └──┘                └┘ └──┘
st   ───────────────────────────────────┘└─
112    simp only [this, geom_sum hx1'] {eta := ff},
id                └──┘  └──────┘ └──┘          └┘
src    └─────────┘    └┘└──────┘    └┘ └─────┘└┘
typ    └─────────┘└──┘└┘└──────┘└──┘└┘ └─────┘└┘
doc    └─────────┘    └┘            └┘ └─────┘  
txt    └─────────┘    └┘            └┘ └─────┘  
par    └─────────┘    └┘            └┘ └─────┘  
pid        └──┘└┘    └┘             └─────┘  
st   ────────────────────────────────────────────┘└─
113    conv in (_ / _) { rw [← neg_div_neg_eq, neg_sub, neg_sub] },
id                            └────────────┘  └─────┘  └─────┘
src    └──────┘ └┘└────┘└────┘└────────────┘└┘└─────┘└┘└─────┘└┘
typ    └──────┘ └┘└────┘└────┘└────────────┘└┘└─────┘└┘└─────┘└┘
txt    └──────┘ └┘ └────┘└────┘              └┘       └┘       └┘
par    └──────┘ └┘ └────┘└────┘              └┘       └┘       └┘
pid        └─┘ └┘ └─┘└───────┘              └┘       └┘       └─┘
st   ──────────────────┘└───────────────────┘└───────┘└───────┘ └┘
114    refine @is_cau_of_mono_bounded _ _ _ _ ((1 : α) / (1 - abv x)) 0 _ _,
id             └────────────────────┘                       └─┘ 
src    └─────┘ └────────────────────┘└───────┘  └──┘ └┘  └┘    └──────┘
typ    └─────┘ └────────────────────┘└───────┘  └──┘└┘  └┘└─┘└──────┘
doc    └─────┘                       └───────┘  └──┘ └┘  └┘     └──────┘
txt    └─────┘                       └───────┘  └──┘ └┘  └┘     └──────┘
par    └─────┘                       └───────┘  └──┘ └┘  └┘     └──────┘
pid                                 └───────┘  └──┘ └┘  └┘     └──────┘
st   ─────────────────────────────────────────────────────────────────────┘└─
115    { assume n hn,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ───┘└─────────┘└─
116      rw abs_of_nonneg,
id          └───────────┘
src      └─┘└───────────┘
typ      └─┘└───────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───────────────────┘└─
117      refine div_le_div_of_le_of_pos (sub_le_self _ (abv_pow abv x n ▸ abv_nonneg _ _))
id              └─────────────────────┘  └─────────┘    └─────┘ └─┘    └────────┘
src      └─────┘└─────────────────────┘ └─────────┘└─┘ └─────┘     └────────┘└──────
typ      └─────┘└─────────────────────┘ └─────────┘└─┘ └─────┘└─┘└────────┘└──────
doc      └─────┘                                   └─┘                        └──────
txt      └─────┘                                   └─┘                        └──────
par      └─────┘                                   └─┘                        └──────
pid                                               └─┘                        └──────
st   ──────────────────────────────────────────────────────────────────────────────────────
118        (sub_pos.2 hx1),
id          └─────┘   └─┘
src  ─────┘ └─────┘└─┘   
typ  ─────┘ └─────┘└─┘└─┘
doc  ─────┘        └─┘   
txt  ─────┘        └─┘   
par  ─────┘        └─┘   
pid  ─────┘        └─┘   
st   ────────────────────┘└─
119      refine div_nonneg (sub_nonneg.2 _) (sub_pos.2 hx1),
id              └────────┘  └────────┘       └─────┘   └─┘
src      └─────┘└────────┘ └────────┘└────┘ └─────┘└─┘   
typ      └─────┘└────────┘ └────────┘└────┘ └─────┘└─┘└─┘
doc      └─────┘                     └────┘        └─┘   
txt      └─────┘                     └────┘        └─┘   
par      └─────┘                     └────┘        └─┘   
pid                                 └────┘        └─┘   
st   ─────────────────────────────────────────────────────┘└─
120      clear hn,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid           └─┘
st   ───────────┘└─
121      induction n with n ih,
id                 
src      └────────┘ └────────┘
typ      └────────┘└────────┘
doc      └────────┘ └────────┘
txt      └────────┘ └────────┘
par      └────────┘ └────────┘
pid                └───────┘
st   ────────────────────────┘└─
122      { simp },
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid            
st   ─────┘└───┘└┘
123      { rw [_root_.pow_succ, ← one_mul (1 : α)],
id             └─────────────┘    └─────┘      
src        └──┘└─────────────┘└──┘└─────┘ └──┘ └┘
typ        └──┘└─────────────┘└──┘└─────┘ └──┘└┘
doc        └──┘               └──┘        └──┘ └┘
txt        └──┘               └──┘        └──┘ └┘
par        └──┘               └──┘        └──┘ └┘
pid          └┘               └──┘        └──┘ └┘
st   ────────────────────────┘└─────────────────┘└─
124        refine mul_le_mul (le_of_lt hx1) ih (abv_pow abv x n ▸ abv_nonneg _ _) (by norm_num) } },
id                └────────┘  └──────┘ └─┘  └┘  └─────┘ └─┘     └────────┘
src        └─────┘└────────┘ └──────┘   └┘   └─────┘      └────────┘└────┘   └──────┘└┘
typ        └─────┘└────────┘ └──────┘└─┘└┘└┘ └─────┘└─┘ └────────┘└────┘   └──────┘└┘
doc        └─────┘                      └┘                          └────┘   └──────┘└┘
txt        └─────┘                      └┘                          └────┘   └──────┘└┘
par        └─────┘                      └┘                          └────┘   └──────┘└┘
pid                                    └┘                          └────┘   └────────┘
st   ───────────────────────────────────────────────────────────────────────────────┘└───────┘└┘└──┘
125    { assume n hn,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ──────────────┘└─
126      refine div_le_div_of_le_of_pos (sub_le_sub_left _ _) (sub_pos.2 hx1),
id              └─────────────────────┘  └─────────────┘       └─────┘   └─┘
src      └─────┘└─────────────────────┘ └─────────────┘└────┘ └─────┘└─┘   
typ      └─────┘└─────────────────────┘ └─────────────┘└────┘ └─────┘└─┘└─┘
doc      └─────┘                                       └────┘        └─┘   
txt      └─────┘                                       └────┘        └─┘   
par      └─────┘                                       └────┘        └─┘   
pid                                                   └────┘        └─┘   
st   ───────────────────────────────────────────────────────────────────────┘└─
127      rw [← one_mul (_ ^ n), _root_.pow_succ],
id             └─────┘         └─────────────┘
src      └────┘└─────┘ └┘  └─┘└─────────────┘
typ      └────┘└─────┘ └┘ └─┘└─────────────┘
doc      └────┘        └┘  └─┘               
txt      └────┘        └┘  └─┘               
par      └────┘        └┘  └─┘               
pid        └──┘        └┘  └─┘               
st   ────────────────────────┘└───────────────┘└──
128      exact mul_le_mul_of_nonneg_right (le_of_lt hx1) (pow_nonneg (abv_nonneg _ _) _) }
id             └────────────────────────┘  └──────┘ └─┘   └────────┘  └────────┘
src      └────┘└────────────────────────┘ └──────┘   └┘ └────────┘ └────────┘└───────┘
typ      └────┘└────────────────────────┘ └──────┘└─┘└┘ └────────┘ └────────┘└───────┘
doc      └────┘                                      └┘                      └───────┘
txt      └────┘                                      └┘                      └───────┘
par      └────┘                                      └┘                      └───────┘
pid                                                 └┘                      └──────┘
st   ───────────────────────────────────────────────────────────────────────────────────┘└─
129  end
st   ──┘
130  
131  lemma is_cau_geo_series_const (a : α) {x : α} (hx1 : abs x < 1) : is_cau_seq abs (λ m, (range m).sum (λ n, a * x ^ n)) :=
id                                                      └─┘        └────────┘ └─┘       └───┘  └─┘           
src                                                       └─┘         └────────┘ └─┘        └───┘   └─┘             
typ                                                     └─┘        └────────┘ └─┘       └───┘  └─┘           
doc                                                                    └────────┘            └───┘
132  have is_cau_seq abs (λ m, a * (range m).sum (λ n, x ^ n)) := (cau_seq.const abs a * ⟨_, is_cau_geo_series x hx1⟩).2,
id        └────────┘ └─┘         └───┘  └─┘                └───────────┘ └─┘       └───────────────┘  └─┘  
src       └────────┘ └─┘           └───┘   └─┘                   └───────────┘ └─┘        └───────────────┘        
typ       └────────┘ └─┘         └───┘  └─┘                └───────────┘ └─┘       └───────────────┘  └─┘  
doc       └────────┘                └───┘                          └───────────┘
133    by simpa only [mul_sum]
id                    └─────┘
src       └──────────┘└─────┘└─
typ       └──────────┘└─────┘└─
doc       └──────────┘       └─
txt       └──────────┘       └─
par       └──────────┘       └─
pid            └──┘└┘       
st       └─────────────────────
134  
src  
typ  
doc  
txt  
par  
pid  
st   
135  lemma series_ratio_test {f : ℕ → β} (n : ℕ) (r : α)
id                                                 
src                                          
typ                                                
136    (hr0 : 0 ≤ r) (hr1 : r < 1) (h : ∀ m, n ≤ m → abv (f m.succ) ≤ r * abv (f m)) :
id                                           └─┘   └───┘     └─┘   
src                                                       └───┘     
typ                                          └─┘   └───┘     └─┘   
137    is_cau_seq abv (λ m, (range m).sum f) :=
id     └────────┘ └─┘       └───┘  └─┘  
src    └────────┘            └───┘   └─┘
typ    └────────┘ └─┘       └───┘  └─┘  
doc    └────────┘            └───┘
138  have har1 : abs r < 1, by rwa abs_of_nonneg hr0,
id               └─┘             └───────────┘ └─┘
src              └─┘          └──┘└───────────┘
typ              └─┘         └──┘└───────────┘└─┘
doc                            └──┘             
txt                            └──┘             
par                            └──┘             
pid                                            
st                            └────────────────────┘
139  begin
st   └─────
140    refine is_cau_series_of_abv_le_cau n.succ _ (is_cau_geo_series_const (abv (f n.succ) * r⁻¹ ^ n.succ) har1),
id            └─────────────────────────┘           └─────────────────────┘  └─┘            └┘  └────┘  └──┘
src    └─────┘└─────────────────────────┘      └─┘ └─────────────────────┘            └┘ └┘└────┘└┘    
typ    └─────┘└─────────────────────────┘      └─┘ └─────────────────────┘ └─┘       └┘└┘└────┘└┘└──┘
doc    └─────┘                                 └─┘                                    └┘           └┘    
txt    └─────┘                                 └─┘                                    └┘           └┘    
par    └─────┘                                 └─┘                                    └┘           └┘    
pid                                           └─┘                                    └┘           └┘    
st   ───────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
141    assume m hmn,
src    └──────────┘
typ    └──────────┘
doc    └──────────┘
txt    └──────────┘
par    └──────────┘
pid    └──────────┘
st   ─────────────┘└─
142    cases classical.em (r = 0) with r_zero r_ne_zero,
id           └──────────┘   
src    └────┘└──────────┘  └───────────────────────┘
typ    └────┘└──────────┘ └───────────────────────┘
doc    └────┘               └───────────────────────┘
txt    └────┘               └───────────────────────┘
par    └────┘               └───────────────────────┘
pid                        └─┘└────────────────────┘
st   ─────────────────────────────────────────────────┘└─
143    { have m_pos := lt_of_lt_of_le (nat.succ_pos n) hmn,
id                     └────────────┘  └──────────┘   └─┘
src      └────────────┘└────────────┘ └──────────┘ └┘
typ      └────────────┘└────────────┘ └──────────┘└┘└─┘
doc      └────────────┘                            └┘
txt      └────────────┘                            └┘
par      └────────────┘                            └┘
pid      └────────┘└─┘                            └┘
st   ───┘└───────────────────────────────────────────────┘└─
144      have := h m.pred (nat.le_of_succ_le_succ (by rwa [nat.succ_pred_eq_of_pos m_pos])),
id                └────┘  └────────────────────┘          └─────────────────────┘ └───┘
src      └──────┘ └────┘ └────────────────────┘   └───┘└─────────────────────┘     └┘
typ      └──────┘└────┘ └────────────────────┘   └───┘└─────────────────────┘└───┘└┘
doc      └──────┘                                 └───┘                            └┘
txt      └──────┘                                 └───┘                            └┘
par      └──────┘                                 └───┘                            └┘
pid      └───┘└─┘                                 └────┘                            └─┘
st   ───────────────────────────────────────────────┘└─────────────────────────────────┘└┘└─
145      simpa [r_zero, nat.succ_pred_eq_of_pos m_pos, pow_succ] },
id              └────┘  └─────────────────────┘ └───┘  └──────┘
src      └─────┘      └┘└─────────────────────┘     └┘└──────┘└┘
typ      └─────┘└────┘└┘└─────────────────────┘└───┘└┘└──────┘└┘
doc      └─────┘      └┘                            └┘        └┘
txt      └─────┘      └┘                            └┘        └┘
par      └─────┘      └┘                            └┘        └┘
pid                 └┘                            └┘        
st   ───────────────────────────────────────────────────────────┘└┘
146    generalize hk : m - n.succ = k,
id                       └────┘
src    └──────────────┘ └────┘ 
typ    └──────────────┘└────┘ 
doc    └──────────────┘         
txt    └──────────────┘         
par    └──────────────┘         
pid              └─┘└┘         
st   ───────────────────────────────┘└─
147    have r_pos : 0 < r := lt_of_le_of_ne hr0 (ne.symm r_ne_zero),
id                         └────────────┘ └─┘  └─────┘ └───────┘
src    └─────────────┘ └──┘└────────────┘    └─────┘         
typ    └─────────────┘└──┘└────────────┘└─┘ └─────┘└───────┘
doc    └─────────────┘  └──┘                                  
txt    └─────────────┘  └──┘                                  
par    └─────────────┘  └──┘                                  
pid    └────────┘└───┘  └──┘                                  
st   ─────────────────────────────────────────────────────────────┘└─
148    replace hk : m = k + n.succ := (nat.sub_eq_iff_eq_add hmn).1 hk,
id                       └────┘     └───────────────────┘ └─┘    └┘
src    └───────────┘   └────┘└──┘ └───────────────────┘   └──┘
typ    └───────────┘ └────┘└──┘ └───────────────────┘└─┘└──┘└┘
doc    └───────────┘          └──┘                         └──┘
txt    └───────────┘          └──┘                         └──┘
par    └───────────┘          └──┘                         └──┘
pid           └─┘└─┘          └──┘                         └──┘
st   ────────────────────────────────────────────────────────────────┘└─
149    induction k with k ih generalizing m n,
id               
src    └────────┘ └─────────────────────────┘
typ    └────────┘└─────────────────────────┘
doc    └────────┘ └─────────────────────────┘
txt    └────────┘ └─────────────────────────┘
par    └────────┘ └─────────────────────────┘
pid              └───────┘└───────────────┘
st   ───────────────────────────────────────┘└─
150    { rw [hk, zero_add, mul_right_comm, ← pow_inv _ _ r_ne_zero, ← div_eq_mul_inv, mul_div_cancel],
id           └┘  └──────┘  └────────────┘    └─────┘     └───────┘    └────────────┘  └────────────┘
src      └──┘  └┘└──────┘└┘└────────────┘└──┘└─────┘└───┘         └──┘└────────────┘└┘└────────────┘
typ      └──┘└┘└┘└──────┘└┘└────────────┘└──┘└─────┘└───┘└───────┘└──┘└────────────┘└┘└────────────┘
doc      └──┘  └┘        └┘              └──┘       └───┘         └──┘              └┘              
txt      └──┘  └┘        └┘              └──┘       └───┘         └──┘              └┘              
par      └──┘  └┘        └┘              └──┘       └───┘         └──┘              └┘              
pid        └┘  └┘        └┘              └──┘       └───┘         └──┘              └┘              
st   ───┘└────┘└────────┘└──────────────┘└───────────────────────┘└────────────────┘└──────────────┘└─
151      exact (ne_of_lt (pow_pos r_pos _)).symm },
id              └──────┘  └─────┘ └───┘
src      └────┘ └──────┘ └─────┘     └────────┘
typ      └────┘ └──────┘ └─────┘└───┘└────────┘
doc      └────┘                      └────────┘
txt      └────┘                      └────────┘
par      └────┘                      └────────┘
pid                                 └──────┘└┘
st   ───────────────────────────────────────────┘└┘
152    { have kn : k + n.succ ≥ n.succ, by rw ← zero_add n.succ; exact add_le_add (zero_le _) (by simp),
id                            └────┘          └──────┘ └────┘        └────────┘  └─────┘
src      └────────┘        └────┘     └───┘└──────┘└────┘  └────┘└────────┘ └─────┘└──┘   └──┘
typ      └────────┘       └────┘     └───┘└──────┘└────┘  └────┘└────────┘ └─────┘└──┘   └──┘
doc      └────────┘                    └───┘                └────┘                  └──┘   └──┘
txt      └────────┘                    └───┘                └────┘                  └──┘   └──┘
par      └────────┘                    └───┘                └────┘                  └──┘   └──┘
pid      └─────┘└─┘                      └─┘                                       └──┘   └────┘
st   ────────────────────────────────┘                                                           └───┘ └─
153      rw [hk, nat.succ_add, pow_succ' r, ← mul_assoc],
id           └┘  └──────────┘  └───────┘     └───────┘
src      └──┘  └┘└──────────┘└┘└───────┘ └──┘└───────┘
typ      └──┘└┘└┘└──────────┘└┘└───────┘└──┘└───────┘
doc      └──┘  └┘            └┘          └──┘         
txt      └──┘  └┘            └┘          └──┘         
par      └──┘  └┘            └┘          └──┘         
pid        └┘  └┘            └┘          └──┘         
st   ─────────┘└────────────┘└───────────┘└───────────┘└──
154      exact le_trans (by rw mul_comm; exact h _ (nat.le_of_succ_le kn))
id             └──────┘        └──────┘            └───────────────┘ └┘
src      └────┘└──────┘   └─┘└──────┘└──────┘ └─┘ └───────────────┘  └──
typ      └────┘└──────┘   └─┘└──────┘└──────┘└─┘ └───────────────┘└┘└──
doc      └────┘           └─┘        └──────┘ └─┘                    └──
txt      └────┘           └─┘        └──────┘ └─┘                    └──
par      └────┘           └─┘        └──────┘ └─┘                    └──
pid                      └──┘        └──────┘ └─┘                    └──
st   ─────────────────────┘└────────────────────────────────────────────┘└─
155        (mul_le_mul_of_nonneg_right (ih (k + n.succ) n h kn rfl) hr0) }
id          └────────────────────────┘  └┘     └────┘    └┘ └─┘  └─┘
src  ─────┘ └────────────────────────┘      └────┘└┘    └─┘└┘   └┘
typ  ─────┘ └────────────────────────┘ └┘  └────┘└┘└┘└─┘└┘└─┘└┘
doc  ─────┘                                       └┘       └┘   └┘
txt  ─────┘                                       └┘       └┘   └┘
par  ─────┘                                       └┘       └┘   └┘
pid  ─────┘                                       └┘       └┘   
st   ───────────────────────────────────────────────────────────────────┘└─
156  end
st   ──┘
157  
158  lemma sum_range_diag_flip {α : Type*} [add_comm_monoid α] (n : ℕ) (f : ℕ → ℕ → α) :
id                                          └─────────────┘                     
src                                         └─────────────┘                   
typ                                         └─────────────┘                     
159    (range n).sum (λ m, (range (m + 1)).sum (λ k, f k (m - k))) =
id      └───┘  └─┘        └───┘       └─┘                
src     └───┘   └─┘         └───┘        └─┘                     
typ     └───┘  └─┘        └───┘       └─┘                
doc     └───┘               └───┘
160    (range n).sum (λ m, (range (n - m)).sum (f m)) :=
id      └───┘  └─┘        └───┘      └─┘    
src     └───┘   └─┘         └───┘        └─┘
typ     └───┘  └─┘        └───┘      └─┘    
doc     └───┘               └───┘
161  have h₁ : ((range n).sigma (range ∘ nat.succ)).sum
id               └───┘  └───┘   └───┘  └──────┘  └─┘
src              └───┘   └───┘   └───┘  └──────┘  └─┘
typ              └───┘  └───┘   └───┘  └──────┘  └─┘
doc              └───┘   └───┘   └───┘
162      (λ (a : Σ m, ℕ), f (a.2) (a.1 - a.2)) =
id                                 
src                                     
typ                                
163      (range n).sum (λ m, (range (m + 1)).sum
id        └───┘  └─┘        └───┘       └─┘
src       └───┘   └─┘         └───┘        └─┘
typ       └───┘  └─┘        └───┘       └─┘
doc       └───┘               └───┘
164      (λ k, f k (m - k))) := sum_sigma,
id                        └───────┘
src                            └───────┘
typ                       └───────┘
165  have h₂ : ((range n).sigma (λ m, range (n - m))).sum (λ a : Σ (m : ℕ), ℕ, f (a.1) (a.2)) =
id               └───┘  └───┘       └───┘       └─┘                             
src              └───┘   └───┘        └───┘         └─┘                                
typ              └───┘  └───┘       └───┘       └─┘                             
doc              └───┘   └───┘        └───┘
166      (range n).sum (λ m, sum (range (n - m)) (f m)) := sum_sigma,
id        └───┘  └─┘       └─┘  └───┘               └───────┘
src       └───┘   └─┘        └─┘  └───┘                   └───────┘
typ       └───┘  └─┘       └─┘  └───┘               └───────┘
doc       └───┘                   └───┘
167  h₁ ▸ h₂ ▸ sum_bij
id   └┘  └┘  └─────┘
src          └─────┘
typ  └┘  └┘  └─────┘
168  (λ a _, ⟨a.2, a.1 - a.2⟩)
id                
src                    
typ               
169  (λ a ha, have h₁ : a.1 < n := mem_range.1 (mem_sigma.1 ha).1,
id       └┘                   └───────┘   └───────┘  └┘ 
src                              └───────┘   └───────┘     
typ      └┘                   └───────┘   └───────┘  └┘ 
170    have h₂ : a.2 < nat.succ a.1 := mem_range.1 (mem_sigma.1 ha).2,
id                  └──────┘      └───────┘   └───────┘  └┘ 
src                  └──────┘       └───────┘   └───────┘     
typ                 └──────┘      └───────┘   └───────┘  └┘ 
171      mem_sigma.2 ⟨mem_range.2 (lt_of_lt_of_le h₂ h₁),
id       └───────┘   └───────┘   └────────────┘ └┘ └┘
src      └───────┘   └───────┘   └────────────┘
typ      └───────┘   └───────┘   └────────────┘ └┘ └┘
172      mem_range.2 ((nat.sub_lt_sub_right_iff (nat.le_of_lt_succ h₂)).2 h₁)⟩)
id       └───────┘    └──────────────────────┘  └───────────────┘ └┘    └┘
src      └───────┘    └──────────────────────┘  └───────────────┘     
typ      └───────┘    └──────────────────────┘  └───────────────┘ └┘    └┘
173  (λ _ _, rfl)
id         └─┘
src          └─┘
typ        └─┘
174  (λ ⟨a₁, a₂⟩ ⟨b₁, b₂⟩ ha hb h,
id      └┘  └┘  └┘  └┘  └┘ └┘ 
typ     └┘  └┘  └┘  └┘  └┘ └┘ 
175    have ha : a₁ < n ∧ a₂ ≤ a₁ :=
id                        
src                        
typ                       
176        ⟨mem_range.1 (mem_sigma.1 ha).1, nat.le_of_lt_succ (mem_range.1 (mem_sigma.1 ha).2)⟩,
id          └───────┘   └───────┘  └┘    └───────────────┘  └───────┘   └───────┘  └┘ 
src         └───────┘   └───────┘        └───────────────┘  └───────┘   └───────┘     
typ         └───────┘   └───────┘  └┘    └───────────────┘  └───────┘   └───────┘  └┘ 
177    have hb : b₁ < n ∧ b₂ ≤ b₁ :=
id                        
src                        
typ                       
178        ⟨mem_range.1 (mem_sigma.1 hb).1, nat.le_of_lt_succ (mem_range.1 (mem_sigma.1 hb).2)⟩,
id          └───────┘   └───────┘  └┘    └───────────────┘  └───────┘   └───────┘  └┘ 
src         └───────┘   └───────┘        └───────────────┘  └───────┘   └───────┘     
typ         └───────┘   └───────┘  └┘    └───────────────┘  └───────┘   └───────┘  └┘ 
179    have h : a₂ = b₂ ∧ _ := sigma.mk.inj h,
id                           └──────────┘ 
src                          └──────────┘
typ                          └──────────┘ 
180    have h' : a₁ = b₁ - b₂ + a₂ := (nat.sub_eq_iff_eq_add ha.2).1 (eq_of_heq h.2),
id                                  └───────────────────┘ └┘     └───────┘ 
src                                 └───────────────────┘        └───────┘  
typ                                 └───────────────────┘ └┘     └───────┘ 
181    sigma.mk.inj_iff.2
id     └──────────────┘
src    └──────────────┘
typ    └──────────────┘
182      ⟨nat.sub_add_cancel hb.2 ▸ h'.symm ▸ h.1 ▸ rfl,
id        └────────────────┘ └┘   └┘└───┘     └─┘
src       └────────────────┘        └───┘      └─┘
typ       └────────────────┘ └┘   └┘└───┘     └─┘
183        (heq_of_eq h.1)⟩)
id          └───────┘ 
src         └───────┘  
typ         └───────┘ 
184  (λ ⟨a₁, a₂⟩ ha,
id      └┘  └┘  └┘
typ     └┘  └┘  └┘
185    have ha : a₁ < n ∧ a₂ < n - a₁ :=
id                          
src                           
typ                         
186        ⟨mem_range.1 (mem_sigma.1 ha).1, (mem_range.1 (mem_sigma.1 ha).2)⟩,
id          └───────┘   └───────┘  └┘     └───────┘   └───────┘  └┘ 
src         └───────┘   └───────┘         └───────┘   └───────┘     
typ         └───────┘   └───────┘  └┘     └───────┘   └───────┘  └┘ 
187    ⟨⟨a₂ + a₁, a₁⟩, ⟨mem_sigma.2 ⟨mem_range.2 (nat.lt_sub_right_iff_add_lt.1 ha.2),
id                     └───────┘   └───────┘   └─────────────────────────┘  └┘
src                    └───────┘   └───────┘   └─────────────────────────┘    
typ                    └───────┘   └───────┘   └─────────────────────────┘  └┘
188      mem_range.2 (nat.lt_succ_of_le (nat.le_add_left _ _))⟩,
id       └───────┘   └───────────────┘  └─────────────┘
src      └───────┘   └───────────────┘  └─────────────┘
typ      └───────┘   └───────────────┘  └─────────────┘
189    sigma.mk.inj_iff.2 ⟨rfl, heq_of_eq (nat.add_sub_cancel _ _).symm⟩⟩⟩)
id     └──────────────┘   └─┘  └───────┘  └────────────────┘     └──┘
src    └──────────────┘   └─┘  └───────┘  └────────────────┘     └──┘
typ    └──────────────┘   └─┘  └───────┘  └────────────────┘     └──┘
190  
191  lemma abv_sum_le_sum_abv {γ : Type*} (f : γ → β) (s : finset γ) :
id                                                       └────┘ 
src                                                        └────┘
typ                                                      └────┘ 
doc                                                        └────┘
192    abv (s.sum f) ≤ s.sum (abv ∘ f) :=
id     └─┘  └──┘    └──┘  └─┘  
src          └──┘      └──┘      
typ    └─┘  └──┘    └──┘  └─┘  
193  by haveI := classical.dec_eq γ; exact
id               └──────────────┘ 
src     └───────┘└──────────────┘   └────┘
typ     └───────┘└──────────────┘  └────┘
doc     └───────┘                   └────┘
txt     └───────┘                   └────┘
par     └───────┘                   └────┘
pid          └─┘                        
st     └───────────────────────────────────
194  finset.induction_on s (by simp [abv_zero abv])
id   └─────────────────┘            └──────┘ └─┘
src  └─────────────────┘    └────┘└──────┘   └─
typ  └─────────────────┘   └────┘└──────┘└─┘└─
doc  └─────────────────┘    └────┘           └─
txt                         └────┘           └─
par                         └────┘           └─
pid                         └─────┘           └──
st   ────────────────────────┘└──────────────────┘└─
195    (λ a s has ih, by rw [sum_insert has, sum_insert has];
id                           └────────┘ └─┘  └────────┘ └─┘
src  ─┘  └───────────┘  └──┘└────────┘   └┘└────────┘   └─
typ  ─┘  └───────────┘  └──┘└────────┘└─┘└┘└────────┘└─┘└─
doc  ─┘  └───────────┘  └──┘             └┘             └─
txt  ─┘  └───────────┘  └──┘             └┘             └─
par  ─┘  └───────────┘  └──┘             └┘             └─
pid  ─┘  └───────────┘  └───┘             └┘             └──
st   ──────────────────┘└─────────────────┘└──────────────┘└─
196      exact le_trans (abv_add abv _ _) (add_le_add_left ih _))
id             └──────┘  └─────┘ └─┘       └─────────────┘ └┘
src  ─────────┘└──────┘ └─────┘   └────┘ └─────────────┘  └────
typ  ─────────┘└──────┘ └─────┘└─┘└────┘ └─────────────┘└┘└────
doc  ─────────┘                   └────┘                  └────
txt  ─────────┘                   └────┘                  └────
par  ─────────┘                   └────┘                  └────
pid  ─────────┘                   └────┘                  └──┘
st   ──────────────────────────────────────────────────────────┘└─
197  
src  
typ  
doc  
txt  
par  
pid  
st   
198  lemma sum_range_sub_sum_range {α : Type*} [add_comm_group α] {f : ℕ → α}
id                                              └────────────┘           
src                                             └────────────┘         
typ                                             └────────────┘           
199    {n m : ℕ} (hnm : n ≤ m) : (range m).sum f - (range n).sum f =
id                            └───┘  └─┘     └───┘  └─┘   
src                             └───┘   └─┘      └───┘   └─┘    
typ                           └───┘  └─┘     └───┘  └─┘   
doc                               └───┘             └───┘
200    ((range m).filter (λ k, n ≤ k)).sum f :=
id       └───┘  └────┘           └─┘  
src      └───┘   └────┘              └─┘
typ      └───┘  └────┘           └─┘  
doc      └───┘   └────┘
201  begin
st   └─────
202    rw [← sum_sdiff (@filter_subset _ (λ k, n ≤ k) _ (range m)),
id           └───────┘   └───────────┘                 └───┘ 
src    └────┘└───────┘  └───────────┘└─┘  └──┘  └──┘ └───┘ └───
typ    └────┘└───────┘  └───────────┘└─┘  └──┘ └──┘ └───┘└───
doc    └────┘                        └─┘  └──┘   └──┘ └───┘ └───
txt    └────┘                        └─┘  └──┘   └──┘       └───
par    └────┘                        └─┘  └──┘   └──┘       └───
pid      └──┘                        └─┘  └──┘   └──┘       └───
st   ────────────────────────────────────────────────────────────┘└─
203      sub_eq_iff_eq_add, ← eq_sub_iff_add_eq, add_sub_cancel'],
id       └───────────────┘    └───────────────┘  └─────────────┘
src  ───┘└───────────────┘└──┘└───────────────┘└┘└─────────────┘
typ  ───┘└───────────────┘└──┘└───────────────┘└┘└─────────────┘
doc  ───┘                 └──┘                 └┘               
txt  ───┘                 └──┘                 └┘               
par  ───┘                 └──┘                 └┘               
pid  ───┘                 └──┘                 └┘               
st   ────────────────────┘└───────────────────┘└───────────────┘└──
204    refine finset.sum_congr
id            └──────────────┘
src    └─────┘└──────────────┘
typ    └─────┘└──────────────┘
doc    └─────┘                
txt    └─────┘                
par    └─────┘                
pid                          
st   ──────────────────────────
205      (finset.ext.2 $ λ a, ⟨λ h, by simp at *; finish,
id        └────────┘
src  ───┘ └────────┘└─┘  └──┘  └──┘  └───────┘└┘└────┘└─
typ  ───┘ └────────┘└─┘  └──┘  └──┘  └───────┘└┘└────┘└─
doc  ───┘           └─┘  └──┘  └──┘  └───────┘└┘└────┘└─
txt  ───┘           └─┘  └──┘  └──┘  └───────┘└┘└────┘└─
par  ───┘           └─┘  └──┘  └──┘  └───────┘└┘└────┘└─
pid  ───┘           └─┘  └──┘  └──┘  └───────────────────
st   ────────────────────────────────┘└────────────────┘└─
206      λ h, have ham : a < m := lt_of_lt_of_le (mem_range.1 h) hnm,
id                              └────────────┘  └───────┘      └─┘
src  ───┘ └──┘    └─────┘  └──┘└────────────┘ └───────┘└─┘ └┘   └─
typ  ───┘ └──┘    └─────┘ └──┘└────────────┘ └───────┘└─┘ └┘└─┘└─
doc  ───┘ └──┘    └─────┘   └──┘                        └─┘ └┘   └─
txt  ───┘ └──┘    └─────┘   └──┘                        └─┘ └┘   └─
par  ───┘ └──┘    └─────┘   └──┘                        └─┘ └┘   └─
pid  ───┘ └──┘    └─────┘   └──┘                        └─┘ └┘   └─
st   ─────────────────────────────────────────────────────────────────
207        by simp * at *⟩)
src  ─────┘  └─────────┘└──
typ  ─────┘  └─────────┘└──
doc  ─────┘  └─────────┘└──
txt  ─────┘  └─────────┘└──
par  ─────┘  └─────────┘└──
pid  ─────┘  └──────────────
st   ───────┘└──────────┘└──
208      (λ _ _, rfl),
id               └─┘
src  ───┘  └────┘└─┘
typ  ───┘  └────┘└─┘
doc  ───┘  └────┘   
txt  ───┘  └────┘   
par  ───┘  └────┘   
pid  ───┘  └────┘   
st   ───────────────┘└─
209  end
st   ──┘
210  
211  lemma cauchy_product {a b : ℕ → β}
id                                  
src                              
typ                                 
212    (ha : is_cau_seq abs (λ m, (range m).sum (λ n, abv (a n))))
id           └────────┘ └─┘       └───┘  └─┘       └─┘   
src          └────────┘ └─┘        └───┘   └─┘
typ          └────────┘ └─┘       └───┘  └─┘       └─┘   
doc          └────────┘            └───┘
213    (hb : is_cau_seq abv (λ m, (range m).sum b)) (ε : α) (ε0 : 0 < ε) :
id           └────────┘ └─┘       └───┘  └─┘                     
src          └────────┘            └───┘   └─┘                      
typ          └────────┘ └─┘       └───┘  └─┘                     
doc          └────────┘            └───┘
214    ∃ i : ℕ, ∀ j ≥ i, abv ((range j).sum a * (range j).sum b -
id                  └─┘   └───┘  └─┘     └───┘  └─┘   
src                         └───┘   └─┘      └───┘   └─┘    
typ                 └─┘   └───┘  └─┘     └───┘  └─┘   
doc                            └───┘             └───┘
215    (range j).sum (λ n, (range (n + 1)).sum (λ m, a m * b (n - m)))) < ε :=
id      └───┘  └─┘        └───┘       └─┘                    
src     └───┘   └─┘         └───┘        └─┘                         
typ     └───┘  └─┘        └───┘       └─┘                    
doc     └───┘               └───┘
216  let ⟨Q, hQ⟩ := cau_seq.bounded ⟨_, hb⟩ in
id   └─┘    └┘     └─────────────┘     └┘
src                 └─────────────┘
typ  └─┘    └┘     └─────────────┘     └┘
217  let ⟨P, hP⟩ := cau_seq.bounded ⟨_, ha⟩ in
id   └─┘    └┘     └─────────────┘     └┘
src                 └─────────────┘
typ  └─┘    └┘     └─────────────┘     └┘
218  have hP0 : 0 < P, from lt_of_le_of_lt (abs_nonneg _) (hP 0),
id                         └────────────┘  └────────┘
src                        └────────────┘  └────────┘
typ                        └────────────┘  └────────┘
219  have hPε0 : 0 < ε / (2 * P),
id                       
src                       
typ                      
220    from div_pos ε0 (mul_pos (show (2 : α) > 0, from by norm_num) hP0),
id          └─────┘ └┘  └─────┘                                    └─┘
src         └─────┘     └─────┘                           └──────┘
typ         └─────┘ └┘  └─────┘                          └──────┘  └─┘
doc                                                        └──────┘
txt                                                        └──────┘
par                                                        └──────┘
st                                                        └───────┘
221  let ⟨N, hN⟩ := cau_seq.cauchy₂ ⟨_, hb⟩ hPε0 in
id   └─┘    └┘     └─────────────┘     └┘  └──┘
src                 └─────────────┘
typ  └─┘    └┘     └─────────────┘     └┘  └──┘
222  have hQε0 : 0 < ε / (4 * Q),
id                       
src                       
typ                      
223    from div_pos ε0 (mul_pos (show (0 : α) < 4, by norm_num) (lt_of_le_of_lt (abv_nonneg _ _) (hQ 0))),
id          └─────┘ └┘  └─────┘                                └────────────┘  └────────┘
src         └─────┘     └─────┘                      └──────┘   └────────────┘  └────────┘
typ         └─────┘ └┘  └─────┘                     └──────┘   └────────────┘  └────────┘
doc                                                   └──────┘
txt                                                   └──────┘
par                                                   └──────┘
st                                                   └───────┘
224  let ⟨M, hM⟩ := cau_seq.cauchy₂ ⟨_, ha⟩ hQε0 in
id   └─┘           └─────────────┘     └┘  └──┘
src                 └─────────────┘
typ  └─┘           └─────────────┘     └┘  └──┘
225  ⟨2 * (max N M + 1), λ K hK,
id        └─┘             └┘
src       └─┘     
typ       └─┘             └┘
226  have h₁ : sum (range K) (λ m, (range (m + 1)).sum (λ k, a k * b (m - k))) =
id             └─┘  └───┘         └───┘       └─┘                  
src            └─┘  └───┘           └───┘        └─┘                        
typ            └─┘  └───┘         └───┘       └─┘                  
doc                 └───┘           └───┘
227      sum (range K) (λ m, sum (range (K - m)) (λ n, a m * b n)),
id       └─┘  └───┘        └─┘  └───┘                
src      └─┘  └───┘          └─┘  └───┘                   
typ      └─┘  └───┘        └─┘  └───┘                
doc           └───┘               └───┘
228    by simpa using sum_range_diag_flip K (λ m n, a m * b n),
id                    └─────────────────┘              
src       └──────────┘└─────────────────┘   └────┘    
typ       └──────────┘└─────────────────┘  └────┘  
doc       └──────────┘                      └────┘     
txt       └──────────┘                      └────┘     
par       └──────────┘                      └────┘     
pid            └────┘                      └────┘     
st       └───────────────────────────────────────────────────┘
229  have h₂ : (λ i, (range (K - i)).sum (λ k, a i * b k)) = (λ i, a i * (range (K - i)).sum b),
id                   └───┘      └─┘                        └───┘      └─┘  
src                   └───┘        └─┘                                └───┘        └─┘
typ                  └───┘      └─┘                        └───┘      └─┘  
doc                   └───┘                                               └───┘
230    by simp [finset.mul_sum],
id              └────────────┘
src       └────┘└────────────┘
typ       └────┘└────────────┘
doc       └────┘              
txt       └────┘              
par       └────┘              
pid                         
st       └────────────────────┘
231  have h₃ : (range K).sum (λ i, a i * (range (K - i)).sum b) =
id              └───┘  └─┘           └───┘      └─┘    
src             └───┘   └─┘              └───┘        └─┘     
typ             └───┘  └─┘           └───┘      └─┘    
doc             └───┘                     └───┘
232      (range K).sum (λ i, a i * ((range (K - i)).sum b - (range K).sum b))
id        └───┘  └─┘            └───┘      └─┘     └───┘  └─┘  
src       └───┘   └─┘               └───┘        └─┘      └───┘   └─┘
typ       └───┘  └─┘            └───┘      └─┘     └───┘  └─┘  
doc       └───┘                      └───┘                   └───┘
233      + (range K).sum (λ i, a i * (range K).sum b),
id         └───┘  └─┘           └───┘  └─┘  
src        └───┘   └─┘              └───┘   └─┘
typ        └───┘  └─┘           └───┘  └─┘  
doc         └───┘                     └───┘
234    by rw ← sum_add_distrib; simp [(mul_add _ _ _).symm],
id             └─────────────┘         └─────┘
src       └───┘└─────────────┘  └────┘ └─────┘└───────────┘
typ       └───┘└─────────────┘  └────┘ └─────┘└───────────┘
doc       └───┘                 └────┘        └───────────┘
txt       └───┘                 └────┘        └───────────┘
par       └───┘                 └────┘        └───────────┘
pid         └─┘                             └───────────┘
st       └────────────────────────────────────────────────┘
235  have two_mul_two : (4 : α) = 2 * 2, by norm_num,
id                                
src                                       └──────┘
typ                                      └──────┘
doc                                         └──────┘
txt                                         └──────┘
par                                         └──────┘
st                                         └───────┘
236  have hQ0 : Q ≠ 0, from λ h, by simpa [h, lt_irrefl] using hQε0,
id                                         └───────┘        └──┘
src                                └─────┘ └┘└───────┘└──────┘
typ                               └─────┘└┘└───────┘└──────┘└──┘
doc                                 └─────┘ └┘         └──────┘
txt                                 └─────┘ └┘         └──────┘
par                                 └─────┘ └┘         └──────┘
pid                                       └┘         └────┘
st                                 └──────────────────────────────┘
237  have h2Q0 : 2 * Q ≠ 0, from mul_ne_zero two_ne_zero hQ0,
id                             └─────────┘ └─────────┘ └─┘
src                            └─────────┘ └─────────┘
typ                            └─────────┘ └─────────┘ └─┘
238  have hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε,
id                                            
src                                            
typ                                           
239    by rw [← div_div_eq_div_mul, div_mul_cancel _ (ne.symm (ne_of_lt hP0)),
id              └────────────────┘  └────────────┘    └─────┘  └──────┘ └─┘
src       └────┘└────────────────┘└┘└────────────┘└─┘ └─────┘ └──────┘   └───
typ       └────┘└────────────────┘└┘└────────────┘└─┘ └─────┘ └──────┘└─┘└───
doc       └────┘                  └┘              └─┘                    └───
txt       └────┘                  └┘              └─┘                    └───
par       └────┘                  └┘              └─┘                    └───
pid         └──┘                  └┘              └─┘                    └───
st       └───────────────────────┘└─────────────────────────────────────────┘└─
240      two_mul_two, mul_assoc, ← div_div_eq_div_mul, div_mul_cancel _ h2Q0, add_halves],
id       └─────────┘  └───────┘    └────────────────┘  └────────────┘   └──┘  └────────┘
src  ───┘           └┘└───────┘└──┘└────────────────┘└┘└────────────┘└─┘    └┘└────────┘
typ  ───┘└─────────┘└┘└───────┘└──┘└────────────────┘└┘└────────────┘└─┘└──┘└┘└────────┘
doc  ───┘           └┘         └──┘                  └┘              └─┘    └┘          
txt  ───┘           └┘         └──┘                  └┘              └─┘    └┘          
par  ───┘           └┘         └──┘                  └┘              └─┘    └┘          
pid  ───┘           └┘         └──┘                  └┘              └─┘    └┘          
st   ──────────────┘└─────────┘└────────────────────┘└─────────────────────┘└──────────┘
241  have hNMK : max N M + 1 < K,
id               └─┘         
src              └─┘        
typ              └─┘         
242    from lt_of_lt_of_le (by rw two_mul; exact lt_add_of_pos_left _ (nat.succ_pos _)) hK,
id          └────────────┘        └─────┘        └────────────────┘    └──────────┘     └┘
src         └────────────┘     └─┘└─────┘  └────┘└────────────────┘└─┘ └──────────┘└─┘
typ         └────────────┘     └─┘└─────┘  └────┘└────────────────┘└─┘ └──────────┘└─┘  └┘
doc                            └─┘         └────┘                  └─┘             └─┘
txt                            └─┘         └────┘                  └─┘             └─┘
par                            └─┘         └────┘                  └─┘             └─┘
pid                                                              └─┘             └─┘
st                            └──────────────────────────────────────────────────────┘
243  have hKN : N < K,
id                 
src               
typ                
244    from calc N ≤ max N M : le_max_left _ _
id                   └─┘       └─────────┘
src                  └─┘       └─────────┘
typ                  └─┘       └─────────┘
245    ... < max N M + 1 : nat.lt_succ_self _
id           └─┘          └──────────────┘
src          └─┘          └──────────────┘
typ          └─┘          └──────────────┘
246    ... < K : hNMK,
id              └──┘
typ             └──┘
247  have hsumlesum : (range (max N M + 1)).sum (λ i, abv (a i) *
id                     └───┘  └─┘         └─┘       └─┘     
src                    └───┘  └─┘         └─┘                  
typ                    └───┘  └─┘         └─┘       └─┘     
doc                    └───┘
248      abv ((range (K - i)).sum b - (range K).sum b)) ≤ (range (max N M + 1)).sum
id       └─┘   └───┘      └─┘     └───┘  └─┘       └───┘  └─┘         └─┘
src            └───┘        └─┘      └───┘   └─┘        └───┘  └─┘         └─┘
typ      └─┘   └───┘      └─┘     └───┘  └─┘       └───┘  └─┘         └─┘
doc            └───┘                   └───┘               └───┘
249      (λ i, abv (a i) * (ε / (2 * P))),
id            └─┘            
src                              
typ           └─┘            
250    from sum_le_sum (λ m hmJ, mul_le_mul_of_nonneg_left
id          └────────┘     └─┘  └───────────────────────┘
src         └────────┘           └───────────────────────┘
typ         └────────┘     └─┘  └───────────────────────┘
251      (le_of_lt (hN (K - m) K
id        └──────┘          
src       └──────┘        
typ       └──────┘          
252        (nat.le_sub_left_of_add_le (le_trans
id          └───────────────────────┘  └──────┘
src         └───────────────────────┘  └──────┘
typ         └───────────────────────┘  └──────┘
253          (by rw two_mul; exact add_le_add (le_of_lt (mem_range.1 hmJ))
id                  └─────┘        └────────┘            └───────┘   └─┘
src              └─┘└─────┘  └────┘└────────┘          └───────┘└─┘   └──
typ              └─┘└─────┘  └────┘└────────┘          └───────┘└─┘└─┘└──
doc              └─┘         └────┘                             └─┘   └──
txt              └─┘         └────┘                             └─┘   └──
par              └─┘         └────┘                             └─┘   └──
pid                                                           └─┘   └──
st              └──────────────────────────────────────────────────────────
254            (le_trans (le_max_left _ _) (le_of_lt (lt_add_one _)))) hK))
id              └──────┘  └─────────┘       └──────┘  └────────┘       └┘
src  ─────────┘ └──────┘ └─────────┘└────┘ └──────┘ └────────┘└───┘
typ  ─────────┘ └──────┘ └─────────┘└────┘ └──────┘ └────────┘└───┘  └┘
doc  ─────────┘                     └────┘                    └───┘
txt  ─────────┘                     └────┘                    └───┘
par  ─────────┘                     └────┘                    └───┘
pid  ─────────┘                     └────┘                    └───┘
st   ───────────────────────────────────────────────────────────────┘
255        (le_of_lt hKN))) (abv_nonneg abv _)),
id          └──────┘ └─┘     └────────┘ └─┘
src         └──────┘         └────────┘
typ         └──────┘ └─┘     └────────┘ └─┘
256  have hsumltP : sum (range (max N M + 1)) (λ n, abv (a n)) < P :=
id                  └─┘  └───┘  └─┘               └─┘      
src                 └─┘  └───┘  └─┘                           
typ                 └─┘  └───┘  └─┘               └─┘      
doc                      └───┘
257    calc sum (range (max N M + 1)) (λ n, abv (a n))
id          └─┘  └───┘  └─┘               └─┘   
src         └─┘  └───┘  └─┘     
typ         └─┘  └───┘  └─┘               └─┘   
doc              └───┘
258        = abs (sum (range (max N M + 1)) (λ n, abv (a n))) :
id           └─┘  └─┘  └───┘  └─┘               └─┘   
src          └─┘  └─┘  └───┘  └─┘     
typ          └─┘  └─┘  └───┘  └─┘               └─┘   
doc                    └───┘
259    eq.symm (abs_of_nonneg (sum_nonneg (λ x h, abv_nonneg abv (a x))))
id     └─────┘  └───────────┘  └────────┘       └────────┘ └─┘   
src    └─────┘  └───────────┘  └────────┘         └────────┘
typ    └─────┘  └───────────┘  └────────┘       └────────┘ └─┘   
260    ... < P : hP (max N M + 1),
id                   └─┘     
src                  └─┘     
typ                  └─┘     
261  begin
st   └─────
262    rw [h₁, h₂, h₃, sum_mul, ← sub_sub, sub_right_comm, sub_self, zero_sub, abv_neg abv],
id         └┘  └┘  └┘  └─────┘    └─────┘  └────────────┘  └──────┘  └──────┘  └─────┘ └─┘
src    └──┘  └┘  └┘  └┘└─────┘└──┘└─────┘└┘└────────────┘└┘└──────┘└┘└──────┘└┘└─────┘   
typ    └──┘└┘└┘└┘└┘└┘└┘└─────┘└──┘└─────┘└┘└────────────┘└┘└──────┘└┘└──────┘└┘└─────┘└─┘
doc    └──┘  └┘  └┘  └┘       └──┘       └┘              └┘        └┘        └┘          
txt    └──┘  └┘  └┘  └┘       └──┘       └┘              └┘        └┘        └┘          
par    └──┘  └┘  └┘  └┘       └──┘       └┘              └┘        └┘        └┘          
pid      └┘  └┘  └┘  └┘       └──┘       └┘              └┘        └┘        └┘          
st   ───────┘└──┘└──┘└───────┘└─────────┘└──────────────┘└────────┘└────────┘└───────────┘└──
263    refine lt_of_le_of_lt (abv_sum_le_sum_abv _ _) _,
id            └────────────┘  └────────────────┘
src    └─────┘└────────────┘ └────────────────┘└─────┘
typ    └─────┘└────────────┘ └────────────────┘└─────┘
doc    └─────┘                                 └─────┘
txt    └─────┘                                 └─────┘
par    └─────┘                                 └─────┘
pid                                           └─────┘
st   ─────────────────────────────────────────────────┘└─
264    suffices : (range (max N M + 1)).sum (λ (i : ℕ), abv (a i) * abv ((range (K - i)).sum b - (range K).sum b)) +
id                                                                                
src    └─────────┘            └───────┘  └────┘ └─┘      └┘              └─────┘         └────┘ └─┘ 
typ    └─────────┘            └───────┘  └────┘ └─┘      └┘              └─────┘         └────┘ └─┘ 
doc    └─────────┘             └───────┘  └────┘ └─┘      └┘               └─────┘         └────┘ └─┘ 
txt    └─────────┘             └───────┘  └────┘ └─┘      └┘               └─────┘         └────┘ └─┘ 
par    └─────────┘             └───────┘  └────┘ └─┘      └┘               └─────┘         └────┘ └─┘ 
pid    └───────┘└┘             └───────┘  └────┘ └─┘      └┘               └─────┘         └────┘ └─┘ 
st   ────────────────────────────────────────────────────────────────────────────────────────────────────────────────
265      ((range K).sum (λ (i : ℕ), abv (a i) * abv ((range (K - i)).sum b - (range K).sum b)) -(range (max N M + 1)).sum
id                                                                                                      └─┘  
src  ───┘        └────┘  └────┘ └─┘      └┘               └─────┘         └────┘ └─┘        └─┘   └────────
typ  ───┘        └────┘  └────┘ └─┘      └┘               └─────┘         └────┘ └─┘        └─┘ └────────
doc  ───┘        └────┘  └────┘ └─┘      └┘               └─────┘         └────┘ └─┘              └────────
txt  ───┘        └────┘  └────┘ └─┘      └┘               └─────┘         └────┘ └─┘              └────────
par  ───┘        └────┘  └────┘ └─┘      └┘               └─────┘         └────┘ └─┘              └────────
pid  ───┘        └────┘  └────┘ └─┘      └┘               └─────┘         └────┘ └─┘              └────────
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
266       (λ (i : ℕ), abv (a i) * abv ((range (K - i)).sum b - (range K).sum b))) < ε / (2 * P) * P + ε / (4 * Q) * (2 * Q),
id                               └─┘                           └───┘                                              
src  ────┘  └────┘ └─┘      └┘               └─────┘   └───┘ └────┘ └──┘  └┘  └┘      └┘  └┘  └┘  
typ  ────┘  └────┘ └─┘     └┘ └─┘           └─────┘   └───┘└────┘└──┘  └┘  └┘    └┘  └┘  └┘ 
doc  ────┘  └────┘ └─┘      └┘               └─────┘   └───┘ └────┘ └──┘    └┘  └┘      └┘  └┘  └┘  
txt  ────┘  └────┘ └─┘      └┘               └─────┘         └────┘ └──┘    └┘  └┘      └┘  └┘  └┘  
par  ────┘  └────┘ └─┘      └┘               └─────┘         └────┘ └──┘    └┘  └┘      └┘  └┘  └┘  
pid  ────┘  └────┘ └─┘      └┘               └─────┘         └────┘ └──┘    └┘  └┘      └┘  └┘  └┘  
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
267    { rw hε at this, simpa [abv_mul abv] },
id          └┘                 └─────┘ └─┘
src      └─┘  └──────┘  └─────┘└─────┘   └┘
typ      └─┘└┘└──────┘  └─────┘└─────┘└─┘└┘
doc      └─┘  └──────┘  └─────┘          └┘
txt      └─┘  └──────┘  └─────┘          └┘
par      └─┘  └──────┘  └─────┘          └┘
pid          └──────┘                 
st   ───┘└───────────┘└────────────────────┘└┘
268    refine add_lt_add (lt_of_le_of_lt hsumlesum
id            └────────┘  └────────────┘ └───────┘
src    └─────┘└────────┘ └────────────┘         
typ    └─────┘└────────┘ └────────────┘└───────┘
doc    └─────┘                                  
txt    └─────┘                                  
par    └─────┘                                  
pid                                            
st   ──────────────────────────────────────────────
269      (by rw [← sum_mul, mul_comm]; exact (mul_lt_mul_left hPε0).mpr hsumltP)) _,
id                 └─────┘  └──────┘          └─────────────┘ └──┘      └─────┘
src  ───┘   └────┘└─────┘└┘└──────┘└┘└────┘ └─────────────┘    └────┘       └──┘
typ  ───┘   └────┘└─────┘└┘└──────┘└──────┘ └─────────────┘└──┘└────┘└─────┘└──┘
doc  ───┘   └────┘       └┘        └┘└────┘                    └────┘       └──┘
txt  ───┘   └────┘       └┘        └┘└────┘                    └────┘       └──┘
par  ───┘   └────┘       └┘        └──────┘                    └────┘       └──┘
pid  ───┘   └─────┘       └┘        └───────┘                    └────┘       └──┘
st   ──────┘└────────────┘└────────┘└────────────────────────────────────────┘└──┘└─
270    rw sum_range_sub_sum_range (le_of_lt hNMK),
id        └─────────────────────┘  └──────┘ └──┘
src    └─┘└─────────────────────┘ └──────┘    
typ    └─┘└─────────────────────┘ └──────┘└──┘
doc    └─┘                                    
txt    └─┘                                    
par    └─┘                                    
pid                                          
st   ───────────────────────────────────────────┘└─
271    exact calc sum ((range K).filter (λ k, max N M + 1 ≤ k))
id                                                        
src    └────┘               └───────┘  └──┘      └─┘ └──
typ    └────┘               └───────┘  └──┘      └─┘ └──
doc    └────┘               └───────┘  └──┘      └─┘  └──
txt    └────┘               └───────┘  └──┘      └─┘  └──
par    └────┘               └───────┘  └──┘      └─┘  └──
pid                        └───────┘  └──┘      └─┘  └──
st   ───────────────────────────────────────────────────────────
272        (λ i, abv (a i) * abv (sum (range (K - i)) b - sum (range K) b))
id                                                                      
src  ─────┘  └──┘      └┘                  └─┘            └┘ └──
typ  ─────┘  └──┘      └┘                  └─┘            └┘└──
doc  ─────┘  └──┘      └┘                  └─┘            └┘ └──
txt  ─────┘  └──┘      └┘                  └─┘            └┘ └──
par  ─────┘  └──┘      └┘                  └─┘            └┘ └──
pid  ─────┘  └──┘      └┘                  └─┘            └┘ └──
st   ───────────────────────────────────────────────────────────────────────
273        ≤ sum ((range K).filter (λ k, max N M + 1 ≤ k)) (λ i, abv (a i) * (2 * Q)) :
id           └─┘   └───┘                └─┘                   └─┘  
src  ─────┘ └─┘  └───┘ └───────┘  └──┘└─┘   └─┘  └─┘  └──┘      └┘  └┘  └────
typ  ─────┘ └─┘  └───┘└───────┘  └──┘└─┘ └─┘  └─┘  └──┘└─┘  └┘  └┘  └────
doc  ─────┘      └───┘ └───────┘  └──┘      └─┘  └─┘  └──┘      └┘  └┘  └────
txt  ─────┘            └───────┘  └──┘      └─┘  └─┘  └──┘      └┘  └┘  └────
par  ─────┘            └───────┘  └──┘      └─┘  └─┘  └──┘      └┘  └┘  └────
pid  ─────┘            └───────┘  └──┘      └─┘  └─┘  └──┘      └┘  └┘  └────
st   ───────────────────────────────────────────────────────────────────────────────────
274      sum_le_sum (λ n hn, begin
id       └────────┘
src  ───┘└────────┘  └─────┘     
typ  ───┘└────────┘  └─────┘     
doc  ───┘            └─────┘     
txt  ───┘            └─────┘     
par  ───┘            └─────┘     
pid  ───┘            └─────┘     
st   ───────────────────────┘└─────
275        refine mul_le_mul_of_nonneg_left _ (abv_nonneg _ _),
id                └───────────────────────┘    └────────┘
src  ─────┘└─────┘└───────────────────────┘└─┘ └────────┘└───┘└─
typ  ────────────┘└───────────────────────┘└─┘ └────────┘└──────
doc  ─────┘└─────┘                         └─┘           └───┘└─
txt  ─────┘└─────┘                         └─┘           └───┘└─
par  ────────────┘                         └─┘           └──────
pid  ────────────┘                         └─┘           └──────
st   ────────────────────────────────────────────────────────┘└─
276        rw sub_eq_add_neg,
id            └────────────┘
src  ─────┘└─┘└────────────┘└─
typ  ─────┘└─┘└────────────┘└─
doc  ─────┘└─┘              └─
txt  ─────┘└─┘              └─
par  ─────┘└─┘              └─
pid  ────────┘              └─
st   ──────────────────────┘└─
277        refine le_trans (abv_add _ _ _) _,
id                └──────┘  └─────┘
src  ─────┘└─────┘└──────┘ └─────┘└───────┘└─
typ  ────────────┘└──────┘ └─────┘└──────────
doc  ─────┘└─────┘                └───────┘└─
txt  ─────┘└─────┘                └───────┘└─
par  ────────────┘                └──────────
pid  ────────────┘                └──────────
st   ──────────────────────────────────────┘└─
278        rw [two_mul, abv_neg abv],
id                              └─┘
src  ─────┘└──┘
typ  ─────┘└──┘                 └─┘
doc  ─────┘└──┘
txt  ─────┘└──┘
par  ─────┘└──┘
pid  ─────────┘
st   ─────────┘
279        exact add_le_add (le_of_lt (hQ _)) (le_of_lt (hQ _)),
280      end)
st       └─┘
281      ... < ε / (4 * Q) * (2 * Q) :
id                               
typ                              
282        by rw [← sum_mul, ← sum_range_sub_sum_range (le_of_lt hNMK)];
283        refine (mul_lt_mul_right $ by rw two_mul;
284          exact add_pos (lt_of_le_of_lt (abv_nonneg _ _) (hQ 0))
285            (lt_of_le_of_lt (abv_nonneg _ _) (hQ 0))).2
286          (lt_of_le_of_lt (le_abs_self _)
287            (hM _ _ (le_trans (nat.le_succ_of_le (le_max_right _ _)) (le_of_lt hNMK))
288              (nat.le_succ_of_le (le_max_right _ _))))
289  end⟩
st   └─┘
290  
291  end
292  
293  open finset
294  
295  open cau_seq
296  
297  namespace complex
298  
299  lemma is_cau_abs_exp (z : ℂ) : is_cau_seq _root_.abs
id                             
src                            
typ                            
300    (λ n, (range n).sum (λ m, abs (z ^ m / nat.fact m))) :=
id                            └┘         └┘  └┘   
src                              └┘           └┘  └┘
typ                           └┘         └┘  └┘   
doc                                           └┘  └┘
301  let ⟨n, hn⟩ := exists_nat_gt (abs z) in
id                                   
src                                  
typ                                  
302  have hn0 : (0 : ℝ) < n, from lt_of_le_of_lt (abs_nonneg _) hn,
id                   
src                  
typ                  
303  series_ratio_test n (complex.abs z / n) (div_nonneg_of_nonneg_of_pos (complex.abs_nonneg _) hn0)
id                          └──┘  └─┘ 
src                         └──┘  └─┘
typ                         └──┘  └─┘ 
304    (by rwa [div_lt_iff hn0, one_mul])
305    (λ m hm,
id         └┘
typ        └┘
306      by rw [abs_abs, abs_abs, nat.fact_succ, pow_succ,
307        mul_comm m.succ, nat.cast_mul, ← div_div_eq_div_mul, mul_div_assoc,
id                  └────┘
src                 └────┘
typ                 └────┘
308        mul_div_right_comm, abs_mul, abs_div, abs_cast_nat];
309      exact mul_le_mul_of_nonneg_right
310        (div_le_div_of_le_left (abs_nonneg _) hn0
311          (nat.cast_le.2 (le_trans hm (nat.le_succ _)))) (abs_nonneg _))
id                                    └┘
typ                                   └┘
312  
313  noncomputable theory
314  
315  lemma is_cau_exp (z : ℂ) : is_cau_seq abs (λ n, (range n).sum (λ m, z ^ m / nat.fact m)) :=
id                                        └┘                               └┘  └┘   
src                                       └┘                                    └┘  └┘
typ                                       └┘                               └┘  └┘   
doc                                                                              └┘  └┘
316    is_cau_series_of_abv_cau (is_cau_abs_exp z)
id                                              
typ                                             
317  
318  def exp' (z : ℂ) : cau_seq ℂ complex.abs := ⟨λ n, (range n).sum (λ m, z ^ m / nat.fact m), is_cau_exp z⟩
id                               └┘  └┘  └┘                                  └┘ └┘                 
src                              └┘  └┘  └┘                                       └┘ └┘  
typ                              └┘  └┘  └┘                                  └┘ └┘                 
doc                                                                                └┘ └┘  
319  
320  def exp (z : ℂ) : ℂ := lim (exp' z)
id                                  
src                   
typ                                 
321  
322  def sin (z : ℂ) : ℂ := ((exp (-z * I) - exp (z * I)) * I) / 2
id                          └┘           └┘           
src                         └┘            └┘            
typ                         └┘           └┘           
323  
324  def cos (z : ℂ) : ℂ := (exp (z * I) + exp (-z * I)) / 2
id                                    └┘       
src                                    └┘        
typ                                   └┘       
325  
326  def tan (z : ℂ) : ℂ := sin z / cos z
id                              └┘  
src                              └┘
typ                             └┘  
327  
328  def sinh (z : ℂ) : ℂ := (exp z - exp (-z)) / 2
id                                └┘    
src                                └┘
typ                               └┘    
329  
330  def cosh (z : ℂ) : ℂ := (exp z + exp (-z)) / 2
id                                └┘    
src                                └┘
typ                               └┘    
331  
332  def tanh (z : ℂ) : ℂ := sinh z / cosh z
id                          └┘        
src                         └┘        
typ                         └┘        
333  
334  end complex
335  
336  namespace real
337  
338  open complex
339  
340  def exp (x : ℝ) : ℝ := (exp x).re
id                             └┘
src                             └┘
typ                            └┘
341  
342  def sin (x : ℝ) : ℝ := (sin x).re
id                          └┘  
src                         └┘   
typ                         └┘  
343  
344  def cos (x : ℝ) : ℝ := (cos x).re
id                         └┘   
src                        └┘    
typ                        └┘   
345  
346  def tan (x : ℝ) : ℝ := (tan x).re
id                             └┘
src                             └┘
typ                            └┘
347  
348  def sinh (x : ℝ) : ℝ := (sinh x).re
id                            └┘  └┘
src                           └┘   └┘
typ                           └┘  └┘
349  
350  def cosh (x : ℝ) : ℝ := (cosh x).re
id                          └┘    └┘
src                         └┘     └┘
typ                         └┘    └┘
351  
352  def tanh (x : ℝ) : ℝ := (tanh x).re
id                            └┘  └┘
src                           └┘   └┘
typ                           └┘  └┘
353  
354  end real
355  
356  namespace complex
357  
358  variables (x y : ℂ)
id                    
src                   
typ                   
359  
360  @[simp] lemma exp_zero : exp 0 = 1 :=
id                            └─┘   
src                           └─┘   
typ                           └─┘   
doc    └──┘
361  lim_eq_of_equiv_const $
id   └───────────────────┘
src  └───────────────────┘
typ  └───────────────────┘
362    λ ε ε0, ⟨1, λ j hj, begin
id        └┘         └┘
typ       └┘         └┘
st                         └─────
363    convert ε0,
id             └┘
src    └──────┘
typ    └──────┘└┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid           
st   ───────────┘└─
364    cases j,
id           
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ────────┘└─
365    { exact absurd hj (not_le_of_gt zero_lt_one) },
id             └────┘ └┘  └──────────┘ └─────────┘
src      └────┘└────┘   └──────────┘└─────────┘└┘
typ      └────┘└────┘└┘ └──────────┘└─────────┘└┘
doc      └────┘                                └┘
txt      └────┘                                └┘
par      └────┘                                └┘
pid                                           
st   ───┘└─────────────────────────────────────────┘└┘
366    { dsimp [exp'],
id              └──┘
src      └─────┘└──┘
typ      └─────┘└──┘
doc      └─────┘    
txt      └─────┘    
par      └─────┘    
pid               
st   ───────────────┘└─
367      induction j with j ih,
id                 
typ                
st   ───┘          
368      { dsimp [exp']; simp },
st                            
369      { rw ← ih dec_trivial,
370        simp only [sum_range_succ, pow_succ],
371        simp } }
st              └───
372  end⟩
st   ──┘
373  
374  lemma exp_add : exp (x + y) = exp x * exp y :=
id                   └─┘       └─┘   └─┘ 
src                  └─┘         └─┘    └─┘
typ                  └─┘       └─┘   └─┘ 
375  show lim (⟨_, is_cau_exp (x + y)⟩ : cau_seq ℂ abs) =
id        └─┘      └────────┘         └─────┘  └─┘
src       └─┘      └────────┘           └─────┘  └─┘
typ       └─┘      └────────┘         └─────┘  └─┘
376    lim (show cau_seq ℂ abs, from ⟨_, is_cau_exp x⟩)
id     └─┘       └─────┘  └─┘           └────────┘ 
src    └─┘       └─────┘  └─┘           └────────┘
typ    └─┘       └─────┘  └─┘           └────────┘ 
377    * lim (show cau_seq ℂ abs, from ⟨_, is_cau_exp y⟩),
id      └─┘       └─────┘  └─┘           └────────┘ 
src     └─┘       └─────┘  └─┘           └────────┘
typ     └─┘       └─────┘  └─┘           └────────┘ 
378  from
379  have hj : ∀ j : ℕ, (range j).sum
id                      └───┘  └─┘
src                     └───┘   └─┘
typ                     └───┘  └─┘
doc                      └───┘
380      (λ m, (x + y) ^ m / m.fact) = (range j).sum
id                    └───┘    └───┘  └─┘
src                        └───┘    └───┘   └─┘
typ                   └───┘    └───┘  └─┘
doc                           └───┘     └───┘
381      (λ i, (range (i + 1)).sum (λ k, x ^ k / k.fact *
id             └───┘       └─┘           └───┘ 
src             └───┘        └─┘               └───┘ 
typ            └───┘       └─┘           └───┘ 
doc             └───┘                             └───┘
382      (y ^ (i - k) / (i - k).fact))),
id                    └──┘
src                        └──┘
typ                   └──┘
doc                            └──┘
383    from assume j,
id                 
typ                
384      finset.sum_congr rfl (λ m hm, begin
id       └──────────────┘ └─┘     └┘
src      └──────────────┘ └─┘
typ      └──────────────┘ └─┘     └┘
385        rw [add_pow, div_eq_mul_inv, sum_mul],
386        refine finset.sum_congr rfl (λ i hi, _),
387        have h₁ : (nat.choose m i : ℂ) ≠ 0 := nat.cast_ne_zero.2
388          (nat.pos_iff_ne_zero.1 (nat.choose_pos (nat.le_of_lt_succ (mem_range.1 hi)))),
389        have h₂ := nat.choose_mul_fact_mul_fact (nat.le_of_lt_succ $ finset.mem_range.1 hi),
390        rw [← h₂, nat.cast_mul, nat.cast_mul, mul_inv', mul_inv'],
391        simp only [mul_left_comm (nat.choose m i : ℂ), mul_assoc, mul_left_comm (nat.choose m i : ℂ)⁻¹,
id                                   └────────┘                                   └────────┘  
src                                  └────────┘                                     └────────┘
typ                                  └────────┘                                   └────────┘  
doc                                  └────────┘                                     └────────┘
392          mul_comm (nat.choose m i : ℂ)],
id                     └────────┘  
src                    └────────┘
typ                    └────────┘  
doc                    └────────┘
393        rw inv_mul_cancel h₁,
394        simp [div_eq_mul_inv, mul_comm, mul_assoc, mul_left_comm]
395      end),
st       └─┘
396  by rw lim_mul_lim;
397    exact eq.symm (lim_eq_lim_of_equiv (by dsimp; simp only [hj];
398      exact cauchy_product (is_cau_abs_exp x) (is_cau_exp y)))
id                                                          
typ                                                         
399  
400  attribute [irreducible] complex.exp
id                           └────┘  └─┘
src                          └────┘  └─┘
typ                          └────┘  └─┘
doc             └─────────┘
401  
402  lemma exp_list_sum (l : list ℂ) : exp l.sum = (l.map exp).prod :=
id                             └┘                     └┘
src                            └┘                       └┘
typ                            └┘                     └┘
403  @monoid_hom.map_list_prod (multiplicative ℂ) ℂ _ _ ⟨exp, exp_zero, exp_add⟩ l
id                              └┘  └┘  └┘  └┘          └┘                     
src                             └┘  └┘  └┘  └┘          └┘
typ                             └┘  └┘  └┘  └┘          └┘                     
404  
405  lemma exp_multiset_sum (s : multiset ℂ) : exp s.sum = (s.map exp).prod :=
id                                 └┘  └┘                     └┘
src                                └┘  └┘                       └┘
typ                                └┘  └┘                     └┘
doc                                └┘  └┘
406  @monoid_hom.map_multiset_prod (multiplicative ℂ) ℂ _ _ ⟨exp, exp_zero, exp_add⟩ s
id                                  └┘  └┘  └┘  └┘          └┘                     
src                                 └┘  └┘  └┘  └┘          └┘
typ                                 └┘  └┘  └┘  └┘          └┘                     
407  
408  lemma exp_sum {α : Type*} (s : finset α) (f : α → ℂ) : exp (s.sum f) = s.prod (exp ∘ f) :=
id                                    └┘                 └┘                   └┘    
src                                   └┘                   └┘                      └┘
typ                                   └┘                 └┘                   └┘    
doc                                   └┘
409  @monoid_hom.map_prod α (multiplicative ℂ) ℂ _ _ ⟨exp, exp_zero, exp_add⟩ f s
id                          └┘ └┘  └┘  └┘            └┘                      
src                          └┘ └┘  └┘  └┘            └┘
typ                         └┘ └┘  └┘  └┘            └┘                      
410  
411  lemma exp_nat_mul (x : ℂ) : ∀ n : ℕ, exp(n*x) = (exp x)^n
id                                       └┘       └┘    
src                                      └┘         └┘
typ                                      └┘       └┘    
412  | 0 := by rw [nat.cast_zero, zero_mul, exp_zero, pow_zero]
st                                                            
413  | (nat.succ n) := by rw [pow_succ', nat.cast_add_one, add_mul, exp_add, ←exp_nat_mul, one_mul]
id      └──────┘
src     └──────┘
typ     └──────┘
st                                                                                                
414  
415  lemma exp_ne_zero : exp x ≠ 0 :=
id                       └┘  
src                      └┘
typ                      └┘  
416  λ h, @zero_ne_one ℂ _ $
id                     
src                    
typ                    
417    by rw [← exp_zero, ← add_neg_self x, exp_add, h]; simp
418  
419  lemma exp_neg : exp (-x) = (exp x)⁻¹ :=
id                   └┘         └┘  
src                  └┘          └┘
typ                  └┘         └┘  
420  by rw [← domain.mul_left_inj (exp_ne_zero x), ← exp_add];
421    simp [mul_inv_cancel (exp_ne_zero x)]
id                                       
typ                                      
422  
423  lemma exp_sub : exp (x - y) = exp x / exp y :=
id                   └┘          └┘        
src                  └┘            └┘      
typ                  └┘          └┘        
424  by simp [exp_add, exp_neg, div_eq_mul_inv]
425  
426  @[simp] lemma exp_conj : exp (conj x) = conj (exp x) :=
id                            └┘    └┘      └┘    └┘  
src                           └┘    └┘       └┘    └┘
typ                           └┘    └┘      └┘    └┘  
doc    └──┘
427  begin
428    dsimp [exp],
id            └─┘
src           └─┘
typ           └─┘
429    rw [← lim_conj],
430    refine congr_arg lim (cau_seq.ext (λ _, _)),
id                                          
typ                                         
431    dsimp [exp', function.comp, cau_seq_conj],
432    rw ← sum_hom _ conj,
id                    └──┘
src                   └──┘
typ                   └──┘
433    refine sum_congr rfl (λ n hn, _),
id                             
typ                            
434    rw [conj_div, conj_pow, ← of_real_nat_cast, conj_of_real]
st                                                             
435  end
st   └─┘
436  
437  @[simp] lemma of_real_exp_of_real_re (x : ℝ) : ((exp x).re : ℂ) = exp x :=
id                                                   └┘               
src                                                  └┘             
typ                                                  └┘               
doc    └──┘
438  eq_conj_iff_re.1 $ by rw [← exp_conj, conj_of_real]
439  
440  @[simp] lemma of_real_exp (x : ℝ) : (real.exp x : ℂ) = exp x :=
id                                       └┘  └┘          └┘  
src                                      └┘  └┘           └┘
typ                                      └┘  └┘          └┘  
doc    └──┘
441  of_real_exp_of_real_re _
442  
443  @[simp] lemma exp_of_real_im (x : ℝ) : (exp x).im = 0 :=
id                                          └┘   
src                                         └┘    
typ                                         └┘   
doc    └──┘
444  by rw [← of_real_exp_of_real_re, of_real_im]
445  
446  lemma exp_of_real_re (x : ℝ) : (exp x).re = real.exp x := rfl
id                                  └┘   └┘    └┘  └┘   
src                                 └┘    └┘    └┘  └┘
typ                                 └┘   └┘    └┘  └┘   
447  
448  lemma two_sinh : 2 * sinh x = exp x - exp (-x) :=
id                        └┘      └┘          
src                       └┘       └┘      
typ                       └┘      └┘          
449  mul_div_cancel' _ two_ne_zero'
450  
451  lemma two_cosh : 2 * cosh x = exp x + exp (-x) :=
id                        └┘      └┘          
src                       └┘       └┘      
typ                       └┘      └┘          
452  mul_div_cancel' _ two_ne_zero'
453  
454  @[simp] lemma sinh_zero : sinh 0 = 0 := by simp [sinh]
id                             └┘                     └──┘
src                            └┘                     └──┘
typ                            └┘                     └──┘
doc    └──┘
455  
456  @[simp] lemma sinh_neg : sinh (-x) = -sinh x :=
id                            └┘          └┘   
src                           └┘           └┘
typ                           └┘          └┘   
doc    └──┘
457  by simp [sinh, exp_neg, (neg_div _ _).symm, add_mul]
id            └──┘
src           └──┘
typ           └──┘
458  
459  private lemma sinh_add_aux {a b c d : ℂ} :
id                                         
src                                        
typ                                        
460    (a - b) * (c + d) + (a + b) * (c - d) = 2 * (a * c - b * d) := by ring
id                                                   
typ                                                  
461  
462  lemma sinh_add : sinh (x + y) = sinh x * cosh y + cosh x * sinh y :=
id                    └┘           └┘      └┘      └┘      └┘   
src                   └┘             └┘       └┘       └┘       └┘
typ                   └┘           └┘      └┘      └┘      └┘   
463  begin
464    rw [← domain.mul_left_inj (@two_ne_zero' ℂ _ _ _), two_sinh,
465        exp_add, neg_add, exp_add, eq_comm,
466        mul_add, ← mul_assoc, two_sinh, mul_left_comm, two_sinh,
467        ← domain.mul_left_inj (@two_ne_zero' ℂ _ _ _), mul_add,
468        mul_left_comm, two_cosh, ← mul_assoc, two_cosh],
469    exact sinh_add_aux
470  end
st   └─┘
471  
472  @[simp] lemma cosh_zero : cosh 0 = 1 := by simp [cosh]
id                             └┘                     └──┘
src                            └┘                     └──┘
typ                            └┘                     └──┘
doc    └──┘
473  
474  @[simp] lemma cosh_neg : cosh (-x) = cosh x :=
id                            └┘         └┘   
src                           └┘          └┘
typ                           └┘         └┘   
doc    └──┘
475  by simp [cosh, exp_neg]
id            └──┘
src           └──┘
typ           └──┘
476  
477  private lemma cosh_add_aux {a b c d : ℂ} :
id                                         
src                                        
typ                                        
478    (a + b) * (c + d) + (a - b) * (c - d) = 2 * (a * c + b * d) := by ring
id                                                   
typ                                                  
479  
480  lemma cosh_add : cosh (x + y) = cosh x * cosh y + sinh x * sinh y :=
id                    └┘           └┘      └┘      └┘      └┘   
src                   └┘             └┘       └┘       └┘       └┘
typ                   └┘           └┘      └┘      └┘      └┘   
481  begin
482    rw [← domain.mul_left_inj (@two_ne_zero' ℂ _ _ _), two_cosh,
483        exp_add, neg_add, exp_add, eq_comm,
484        mul_add, ← mul_assoc, two_cosh, ← mul_assoc, two_sinh,
485        ← domain.mul_left_inj (@two_ne_zero' ℂ _ _ _), mul_add,
486        mul_left_comm, two_cosh, mul_left_comm, two_sinh],
487    exact cosh_add_aux
488  end
st   └─┘
489  
490  lemma sinh_sub : sinh (x - y) = sinh x * cosh y - cosh x * sinh y :=
id                    └┘           └┘      └┘      └┘      └┘   
src                   └┘             └┘       └┘       └┘       └┘
typ                   └┘           └┘      └┘      └┘      └┘   
491  by simp [sinh_add, sinh_neg, cosh_neg]
492  
493  lemma cosh_sub : cosh (x - y) = cosh x * cosh y - sinh x * sinh y :=
id                    └┘           └┘      └┘      └┘      └┘   
src                   └┘             └┘       └┘       └┘       └┘
typ                   └┘           └┘      └┘      └┘      └┘   
494  by simp [cosh_add, sinh_neg, cosh_neg]
495  
496  lemma sinh_conj : sinh (conj x) = conj (sinh x) :=
id                     └┘    └┘       └┘    └┘   
src                    └┘    └┘        └┘    └┘
typ                    └┘    └┘       └┘    └┘   
497  by rw [sinh, ← conj_neg, exp_conj, exp_conj, ← conj_sub, sinh, conj_div, conj_two]
st                                                                                    
498  
499  @[simp] lemma of_real_sinh_of_real_re (x : ℝ) : ((sinh x).re : ℂ) = sinh x :=
id                                                    └┘    └┘           
src                                                   └┘     └┘          
typ                                                   └┘    └┘           
doc    └──┘
500  eq_conj_iff_re.1 $ by rw [← sinh_conj, conj_of_real]
501  
502  @[simp] lemma of_real_sinh (x : ℝ) : (real.sinh x : ℂ) = sinh x :=
id                                        └┘  └┘             
src                                       └┘  └┘             
typ                                       └┘  └┘             
doc    └──┘
503  of_real_sinh_of_real_re _
504  
505  @[simp] lemma sinh_of_real_im (x : ℝ) : (sinh x).im = 0 :=
id                                           └┘    └┘
src                                          └┘     └┘
typ                                          └┘    └┘
doc    └──┘
506  by rw [← of_real_sinh_of_real_re, of_real_im]
507  
508  lemma sinh_of_real_re (x : ℝ) : (sinh x).re = real.sinh x := rfl
id                                   └┘    └┘    └┘  └┘   
src                                  └┘     └┘    └┘  └┘  
typ                                  └┘    └┘    └┘  └┘   
509  
510  lemma cosh_conj : cosh (conj x) = conj (cosh x) :=
id                     └┘    └┘       └┘    └┘   
src                    └┘    └┘        └┘    └┘
typ                    └┘    └┘       └┘    └┘   
511  by rw [cosh, ← conj_neg, exp_conj, exp_conj, ← conj_add, cosh, conj_div, conj_two]
st                                                                                    
512  
513  @[simp] lemma of_real_cosh_of_real_re (x : ℝ) : ((cosh x).re : ℂ) = cosh x :=
id                                                    └┘    └┘           
src                                                   └┘     └┘          
typ                                                   └┘    └┘           
doc    └──┘
514  eq_conj_iff_re.1 $ by rw [← cosh_conj, conj_of_real]
515  
516  @[simp] lemma of_real_cosh (x : ℝ) : (real.cosh x : ℂ) = cosh x :=
id                                        └┘  └┘             
src                                       └┘  └┘             
typ                                       └┘  └┘             
doc    └──┘
517  of_real_cosh_of_real_re _
518  
519  @[simp] lemma cosh_of_real_im (x : ℝ) : (cosh x).im = 0 :=
id                                           └┘    └┘
src                                          └┘     └┘
typ                                          └┘    └┘
doc    └──┘
520  by rw [← of_real_cosh_of_real_re, of_real_im]
521  
522  lemma cosh_of_real_re (x : ℝ) : (cosh x).re = real.cosh x := rfl
id                                   └┘    └┘    └┘  └┘   
src                                  └┘     └┘    └┘  └┘  
typ                                  └┘    └┘    └┘  └┘   
523  
524  lemma tanh_eq_sinh_div_cosh : tanh x = sinh x / cosh x := rfl
id                                 └┘      └┘      └┘   
src                                └┘       └┘       └┘
typ                                └┘      └┘      └┘   
525  
526  @[simp] lemma tanh_zero : tanh 0 = 0 := by simp [tanh]
id                             └┘                     └──┘
src                            └┘                     └──┘
typ                            └┘                     └──┘
doc    └──┘
527  
528  @[simp] lemma tanh_neg : tanh (-x) = -tanh x := by simp [tanh, neg_div]
id                            └┘          └┘                └──┘
src                           └┘           └┘                 └──┘
typ                           └┘          └┘                └──┘
doc    └──┘
529  
530  lemma tanh_conj : tanh (conj x) = conj (tanh x) :=
id                     └┘    └┘       └┘    └┘   
src                    └┘    └┘        └┘    └┘
typ                    └┘    └┘       └┘    └┘   
531  by rw [tanh, sinh_conj, cosh_conj, ← conj_div, tanh]
st                                                      
532  
533  @[simp] lemma of_real_tanh_of_real_re (x : ℝ) : ((tanh x).re : ℂ) = tanh x :=
id                                                    └┘    └┘           
src                                                   └┘     └┘          
typ                                                   └┘    └┘           
doc    └──┘
534  eq_conj_iff_re.1 $ by rw [← tanh_conj, conj_of_real]
535  
536  @[simp] lemma of_real_tanh (x : ℝ) : (real.tanh x : ℂ) = tanh x :=
id                                        └┘  └┘             
src                                       └┘  └┘             
typ                                       └┘  └┘             
doc    └──┘
537  of_real_tanh_of_real_re _
538  
539  @[simp] lemma tanh_of_real_im (x : ℝ) : (tanh x).im = 0 :=
id                                           └┘    └┘
src                                          └┘     └┘
typ                                          └┘    └┘
doc    └──┘
540  by rw [← of_real_tanh_of_real_re, of_real_im]
541  
542  lemma tanh_of_real_re (x : ℝ) : (tanh x).re = real.tanh x := rfl
id                                   └┘    └┘    └┘  └┘   
src                                  └┘     └┘    └┘  └┘  
typ                                  └┘    └┘    └┘  └┘   
543  
544  lemma cosh_add_sinh : cosh x + sinh x = exp x :=
id                         └┘      └┘      └┘  
src                        └┘       └┘       └┘
typ                        └┘      └┘      └┘  
545  by rw [← domain.mul_left_inj (@two_ne_zero' ℂ _ _ _), mul_add,
546         two_cosh, two_sinh, add_add_sub_cancel, two_mul]
st                                                         
547  
548  lemma sinh_add_cosh : sinh x + cosh x = exp x :=
id                         └┘      └┘      └┘  
src                        └┘       └┘       └┘
typ                        └┘      └┘      └┘  
549  by rw [add_comm, cosh_add_sinh]
550  
551  lemma cosh_sub_sinh : cosh x - sinh x = exp (-x) :=
id                         └┘      └┘      └┘    
src                        └┘       └┘       └┘
typ                        └┘      └┘      └┘    
552  by rw [← domain.mul_left_inj (@two_ne_zero' ℂ _ _ _), mul_sub,
553         two_cosh, two_sinh, add_sub_sub_cancel, two_mul]
st                                                         
554  
555  lemma cosh_sq_sub_sinh_sq : cosh x ^ 2 - sinh x ^ 2 = 1 :=
id                               └┘          └┘   
src                              └┘           └┘
typ                              └┘          └┘   
556  by rw [sq_sub_sq, cosh_add_sinh, cosh_sub_sinh, ← exp_add, add_neg_self, exp_zero]
st                                                                                    
557  
558  @[simp] lemma sin_zero : sin 0 = 0 := by simp [sin]
id                            └┘                    └─┘
src                           └┘                    └─┘
typ                           └┘                    └─┘
doc    └──┘
559  
560  @[simp] lemma sin_neg : sin (-x) = -sin x :=
id                           └┘         └┘  
src                          └┘          └┘
typ                          └┘         └┘  
doc    └──┘
561  by simp [sin, exp_neg, (neg_div _ _).symm, add_mul]
id            └─┘
src           └─┘
typ           └─┘
562  
563  lemma two_sin : 2 * sin x = (exp (-x * I) - exp (x * I)) * I :=
id                       └┘       └┘          └┘           
src                      └┘        └┘           └┘            
typ                      └┘       └┘          └┘           
564  mul_div_cancel' _ two_ne_zero'
565  
566  lemma two_cos : 2 * cos x = exp (x * I) + exp (-x * I) :=
id                       └┘                └┘       
src                      └┘                  └┘        
typ                      └┘                └┘       
567  mul_div_cancel' _ two_ne_zero'
568  
569  lemma sinh_mul_I : sinh (x * I) = sin x * I :=
id                                 └┘     
src                                 └┘      
typ                                └┘     
570  by rw [← domain.mul_left_inj (@two_ne_zero' ℂ _ _ _), two_sinh,
571         ← mul_assoc, two_sin, mul_assoc, I_mul_I, mul_neg_one,
572         neg_sub, neg_mul_eq_neg_mul]
st                                     
573  
574  lemma cosh_mul_I : cosh (x * I) = cos x :=
id                      └┘           └┘  
src                     └┘            └┘
typ                     └┘           └┘  
575  by rw [← domain.mul_left_inj (@two_ne_zero' ℂ _ _ _), two_cosh,
576         two_cos, neg_mul_eq_neg_mul]
st                                     
577  
578  lemma sin_add : sin (x + y) = sin x * cos y + cos x * sin y :=
id                   └┘          └┘           └┘        
src                  └┘            └┘             └┘      
typ                  └┘          └┘           └┘        
579  by rw [← domain.mul_right_inj I_ne_zero, ← sinh_mul_I,
580         add_mul, add_mul, mul_right_comm, ← sinh_mul_I,
581         mul_assoc, ← sinh_mul_I, ← cosh_mul_I, ← cosh_mul_I, sinh_add]
st                                                                       
582  
583  @[simp] lemma cos_zero : cos 0 = 1 := by simp [cos]
id                            └┘                    └─┘
src                           └┘                    └─┘
typ                           └┘                    └─┘
doc    └──┘
584  
585  @[simp] lemma cos_neg : cos (-x) = cos x :=
id                           └┘        └┘  
src                          └┘         └┘
typ                          └┘        └┘  
doc    └──┘
586  by simp [cos, exp_neg]
id            └─┘
src           └─┘
typ           └─┘
587  
588  private lemma cos_add_aux {a b c d : ℂ} :
id                                        
src                                       
typ                                       
589    (a + b) * (c + d) - (b - a) * (d - c) * (-1) =
id                                 
typ                                
st                                               
590    2 * (a * c + b * d) := by ring
id                   
typ                  
591  
592  lemma cos_add : cos (x + y) = cos x * cos y - sin x * sin y :=
id                   └┘          └┘           └┘        
src                  └┘            └┘             └┘      
typ                  └┘          └┘           └┘        
593  by rw [← cosh_mul_I, add_mul, cosh_add, cosh_mul_I, cosh_mul_I,
594         sinh_mul_I, sinh_mul_I, mul_mul_mul_comm, I_mul_I,
595         mul_neg_one, sub_eq_add_neg]
st                                     
596  
597  lemma sin_sub : sin (x - y) = sin x * cos y - cos x * sin y :=
id                   └┘          └┘           └┘        
src                  └┘            └┘             └┘      
typ                  └┘          └┘           └┘        
598  by simp [sin_add, sin_neg, cos_neg]
599  
600  lemma cos_sub : cos (x - y) = cos x * cos y + sin x * sin y :=
id                   └┘          └┘           └┘        
src                  └┘            └┘             └┘      
typ                  └┘          └┘           └┘        
601  by simp [cos_add, sin_neg, cos_neg]
602  
603  lemma sin_conj : sin (conj x) = conj (sin x) :=
id                    └┘    └┘      └┘    └┘  
src                   └┘    └┘       └┘    └┘
typ                   └┘    └┘      └┘    └┘  
604  by rw [← domain.mul_right_inj I_ne_zero, ← sinh_mul_I,
605         ← conj_neg_I, ← conj_mul, ← conj_mul, sinh_conj,
606         mul_neg_eq_neg_mul_symm, sinh_neg, sinh_mul_I, mul_neg_eq_neg_mul_symm]
st                                                                                
607  
608  @[simp] lemma of_real_sin_of_real_re (x : ℝ) : ((sin x).re : ℂ) = sin x :=
id                                                   └┘               
src                                                  └┘             
typ                                                  └┘               
doc    └──┘
609  eq_conj_iff_re.1 $ by rw [← sin_conj, conj_of_real]
610  
611  @[simp] lemma of_real_sin (x : ℝ) : (real.sin x : ℂ) = sin x :=
id                                       └┘  └┘          └┘  
src                                      └┘  └┘           └┘
typ                                      └┘  └┘          └┘  
doc    └──┘
612  of_real_sin_of_real_re _
613  
614  @[simp] lemma sin_of_real_im (x : ℝ) : (sin x).im = 0 :=
id                                          └┘   
src                                         └┘    
typ                                         └┘   
doc    └──┘
615  by rw [← of_real_sin_of_real_re, of_real_im]
616  
617  lemma sin_of_real_re (x : ℝ) : (sin x).re = real.sin x := rfl
id                                  └┘   └┘    └┘  └┘   
src                                 └┘    └┘    └┘  └┘
typ                                 └┘   └┘    └┘  └┘   
618  
619  lemma cos_conj : cos (conj x) = conj (cos x) :=
id                    └┘    └┘      └┘    └┘  
src                   └┘    └┘       └┘    └┘
typ                   └┘    └┘      └┘    └┘  
620  by rw [← cosh_mul_I, ← conj_neg_I, ← conj_mul, ← cosh_mul_I,
621         cosh_conj, mul_neg_eq_neg_mul_symm, cosh_neg]
st                                                      
622  
623  @[simp] lemma of_real_cos_of_real_re (x : ℝ) : ((cos x).re : ℂ) = cos x :=
id                                                   └┘               
src                                                  └┘             
typ                                                  └┘               
doc    └──┘
624  eq_conj_iff_re.1 $ by rw [← cos_conj, conj_of_real]
625  
626  @[simp] lemma of_real_cos (x : ℝ) : (real.cos x : ℂ) = cos x :=
id                                       └┘  └┘            
src                                      └┘  └┘            
typ                                      └┘  └┘            
doc    └──┘
627  of_real_cos_of_real_re _
628  
629  @[simp] lemma cos_of_real_im (x : ℝ) : (cos x).im = 0 :=
id                                          └┘   └┘
src                                         └┘    └┘
typ                                         └┘   └┘
doc    └──┘
630  by rw [← of_real_cos_of_real_re, of_real_im]
631  
632  lemma cos_of_real_re (x : ℝ) : (cos x).re = real.cos x := rfl
id                                  └┘   └┘    └┘  └┘   
src                                 └┘    └┘    └┘  └┘
typ                                 └┘   └┘    └┘  └┘   
633  
634  @[simp] lemma tan_zero : tan 0 = 0 := by simp [tan]
id                            └┘                    └─┘
src                           └┘                    └─┘
typ                           └┘                    └─┘
doc    └──┘
635  
636  lemma tan_eq_sin_div_cos : tan x = sin x / cos x := rfl
id                              └┘           └┘  
src                             └┘             └┘
typ                             └┘           └┘  
637  
638  @[simp] lemma tan_neg : tan (-x) = -tan x := by simp [tan, neg_div]
id                           └┘         └┘               └─┘
src                          └┘          └┘                └─┘
typ                          └┘         └┘               └─┘
doc    └──┘
639  
640  lemma tan_conj : tan (conj x) = conj (tan x) :=
id                    └┘    └┘      └┘    └┘  
src                   └┘    └┘       └┘    └┘
typ                   └┘    └┘      └┘    └┘  
641  by rw [tan, sin_conj, cos_conj, ← conj_div, tan]
st                                                  
642  
643  @[simp] lemma of_real_tan_of_real_re (x : ℝ) : ((tan x).re : ℂ) = tan x :=
id                                                   └┘               
src                                                  └┘             
typ                                                  └┘               
doc    └──┘
644  eq_conj_iff_re.1 $ by rw [← tan_conj, conj_of_real]
645  
646  @[simp] lemma of_real_tan (x : ℝ) : (real.tan x : ℂ) = tan x :=
id                                       └┘  └┘          └┘  
src                                      └┘  └┘           └┘
typ                                      └┘  └┘          └┘  
doc    └──┘
647  of_real_tan_of_real_re _
648  
649  @[simp] lemma tan_of_real_im (x : ℝ) : (tan x).im = 0 :=
id                                          └┘   
src                                         └┘    
typ                                         └┘   
doc    └──┘
650  by rw [← of_real_tan_of_real_re, of_real_im]
651  
652  lemma tan_of_real_re (x : ℝ) : (tan x).re = real.tan x := rfl
id                                  └┘   └┘    └┘  └┘   
src                                 └┘    └┘    └┘  └┘
typ                                 └┘   └┘    └┘  └┘   
653  
654  lemma cos_add_sin_I : cos x + sin x * I = exp (x * I) :=
id                         └┘              └┘      
src                        └┘                └┘       
typ                        └┘              └┘      
655  by rw [← cosh_add_sinh, sinh_mul_I, cosh_mul_I]
st                                                 
656  
657  lemma cos_sub_sin_I : cos x - sin x * I = exp (-x * I) :=
id                         └┘              └┘       
src                        └┘                └┘        
typ                        └┘              └┘       
658  by rw [← neg_mul_eq_neg_mul, ← cosh_sub_sinh, sinh_mul_I, cosh_mul_I]
st                                                                       
659  
660  lemma sin_sq_add_cos_sq : sin x ^ 2 + cos x ^ 2 = 1 :=
id                             └┘            
src                            └┘          
typ                            └┘            
661  eq.trans
662    (by rw [cosh_mul_I, sinh_mul_I, mul_pow, I_sq, mul_neg_one, sub_neg_eq_add, add_comm])
st                                                                                         
663    (cosh_sq_sub_sinh_sq (x * I))
id                              
src                              
typ                             
664  
665  lemma cos_two_mul' : cos (2 * x) = cos x ^ 2 - sin x ^ 2 :=
id                        └┘           └┘            
src                       └┘            └┘          
typ                       └┘           └┘            
666  by rw [two_mul, cos_add, ← pow_two, ← pow_two]
st                                                
667  
668  lemma cos_two_mul : cos (2 * x) = 2 * cos x ^ 2 - 1 :=
id                       └┘               └┘  
src                      └┘                └┘
typ                      └┘               └┘  
669  by rw [cos_two_mul', eq_sub_iff_add_eq.2 (sin_sq_add_cos_sq x),
670         ← sub_add, sub_add_eq_add_sub, two_mul]
st                                                
671  
672  lemma sin_two_mul : sin (2 * x) = 2 * sin x * cos x :=
id                       └┘               └┘        
src                      └┘                └┘      
typ                      └┘               └┘        
673  by rw [two_mul, sin_add, two_mul, add_mul, mul_comm]
st                                                      
674  
675  lemma cos_square : cos x ^ 2 = 1 / 2 + cos (2 * x) / 2 :=
id                      └┘                         
src                     └┘                  
typ                     └┘                         
676  by simp [cos_two_mul, div_add_div_same, mul_div_cancel_left, two_ne_zero', -one_div_eq_inv]
677  
678  lemma sin_square : sin x ^ 2 = 1 - cos x ^ 2 :=
id                      └┘                
src                     └┘              
typ                     └┘                
679  by { rw [←sin_sq_add_cos_sq x], simp }
st                                        └┘
680  
681  lemma exp_mul_I : exp (x * I) = cos x + sin x * I :=
id                     └┘          └┘           
src                    └┘           └┘             
typ                    └┘          └┘           
682  (cos_add_sin_I _).symm
683  
684  lemma exp_add_mul_I : exp (x + y * I) = exp x * (cos y + sin y * I) :=
id                         └┘             └┘       └┘          
src                        └┘               └┘        └┘            
typ                        └┘             └┘       └┘          
685  by rw [exp_add, exp_mul_I]
st                            
686  
687  lemma exp_eq_exp_re_mul_sin_add_cos : exp x = exp x.re * (cos x.im + sin x.im * I) :=
id                                         └┘        └─┘    └┘  └┘    └┘   └┘   
src                                        └┘          └─┘    └┘   └┘    └┘    └┘   
typ                                        └┘        └─┘    └┘  └┘    └┘   └┘   
688  by rw [← exp_add_mul_I, re_add_im]
689  
690  theorem cos_add_sin_mul_I_pow (n : ℕ) (z : ℂ) : (cos z + sin z * I) ^ n = cos (↑n * z) + sin (↑n * z) * I :=
id                                                  └┘                  └┘           └┘           
src                                                 └┘                     └┘             └┘             
typ                                                 └┘                  └┘           └┘           
691  begin
692    rw [← exp_mul_I, ← exp_mul_I],
693    induction n with n ih,
id               
typ              
694    { rw [pow_zero, nat.cast_zero, zero_mul, zero_mul, exp_zero] },
st                                                                 └┘
695    { rw [pow_succ', ih, nat.cast_succ, add_mul, add_mul, one_mul, exp_add] }
st                                                                            └─
696  end
st   ──┘
697  
698  end complex
699  
700  namespace real
701  
702  open complex
703  
704  variables (x y : ℝ)
id                    
src                   
typ                   
705  
706  @[simp] lemma exp_zero : exp 0 = 1 :=
id                            └─┘   
src                           └─┘   
typ                           └─┘   
doc    └──┘
707  by simp [real.exp]
id            └──────┘
src           └──────┘
typ           └──────┘
st           └──────┘
708  
709  lemma exp_add : exp (x + y) = exp x * exp y :=
id                   └─┘       └─┘   └─┘ 
src                  └─┘         └─┘    └─┘
typ                  └─┘       └─┘   └─┘ 
710  by simp [exp_add, exp]
id            └─────┘  └─┘
src           └─────┘  └─┘
typ           └─────┘  └─┘
st           └─────┘  └─┘
711  
712  lemma exp_list_sum (l : list ℝ) : exp l.sum = (l.map exp).prod :=
id                           └──┘     └─┘ └──┘   └──┘ └─┘ └──┘
src                          └──┘     └─┘  └──┘    └──┘ └─┘ └──┘
typ                          └──┘     └─┘ └──┘   └──┘ └─┘ └──┘
doc                                         └──┘              └──┘
713  @monoid_hom.map_list_prod (multiplicative ℝ) ℝ _ _ ⟨exp, exp_zero, exp_add⟩ l
id    └──────────────────────┘  └────────────┘         └─┘  └──────┘  └─────┘  
src   └──────────────────────┘  └────────────┘         └─┘  └──────┘  └─────┘
typ   └──────────────────────┘  └────────────┘         └─┘  └──────┘  └─────┘  
714  
715  lemma exp_multiset_sum (s : multiset ℝ) : exp s.sum = (s.map exp).prod :=
id                               └──────┘     └─┘ └──┘   └──┘ └─┘ └──┘
src                              └──────┘     └─┘  └──┘    └──┘ └─┘ └──┘
typ                              └──────┘     └─┘ └──┘   └──┘ └─┘ └──┘
doc                              └──────┘                    └──┘     └──┘
716  @monoid_hom.map_multiset_prod (multiplicative ℝ) ℝ _ _ ⟨exp, exp_zero, exp_add⟩ s
id    └──────────────────────────┘  └────────────┘         └─┘  └──────┘  └─────┘  
src   └──────────────────────────┘  └────────────┘         └─┘  └──────┘  └─────┘
typ   └──────────────────────────┘  └────────────┘         └─┘  └──────┘  └─────┘  
717  
718  lemma exp_sum {α : Type*} (s : finset α) (f : α → ℝ) : exp (s.sum f) = s.prod (exp ∘ f) :=
id                                  └────┘               └─┘  └──┘    └───┘  └─┘  
src                                 └────┘                 └─┘   └──┘      └───┘  └─┘ 
typ                                 └────┘               └─┘  └──┘    └───┘  └─┘  
doc                                 └────┘                                   └───┘
719  @monoid_hom.map_prod α (multiplicative ℝ) ℝ _ _ ⟨exp, exp_zero, exp_add⟩ f s
id    └─────────────────┘   └────────────┘         └─┘  └──────┘  └─────┘   
src   └─────────────────┘    └────────────┘         └─┘  └──────┘  └─────┘
typ   └─────────────────┘   └────────────┘         └─┘  └──────┘  └─────┘   
720  
721  lemma exp_nat_mul (x : ℝ) : ∀ n : ℕ, exp(n*x) = (exp x)^n
id                                     └─┘     └─┘  
src                                     └─┘       └─┘   
typ                                    └─┘     └─┘  
722  | 0 := by rw [nat.cast_zero, zero_mul, exp_zero, pow_zero]
id                 └───────────┘  └┘
src                └───────────┘  └┘
typ                └───────────┘  └┘
st                └───────────┘  └┘                          
723  | (nat.succ n) := by rw [pow_succ', nat.cast_add_one, add_mul, exp_add, ←exp_nat_mul, one_mul]
id      └──────┘
src     └──────┘
typ     └──────┘
st                                                                                                
724  
725  lemma exp_ne_zero : exp x ≠ 0 :=
id                       └┘  
src                      └┘
typ                      └┘  
726  λ h, exp_ne_zero x $ by rw [exp, ← of_real_inj] at h; simp * at *
id                    
typ                   
727  
728  lemma exp_neg : exp (-x) = (exp x)⁻¹ :=
id                   └┘         └┘  
src                  └┘          └┘
typ                  └┘         └┘  
729  by rw [← of_real_inj, exp, of_real_exp_of_real_re, of_real_neg, exp_neg,
730    of_real_inv, of_real_exp]
st                             
731  
732  lemma exp_sub : exp (x - y) = exp x / exp y :=
id                   └┘          └┘        
src                  └┘            └┘      
typ                  └┘          └┘        
733  by simp [exp_add, exp_neg, div_eq_mul_inv]
734  
735  @[simp] lemma sin_zero : sin 0 = 0 := by simp [sin]
id                            └┘                    └─┘
src                           └┘                    └─┘
typ                           └┘                    └─┘
doc    └──┘
736  
737  @[simp] lemma sin_neg : sin (-x) = -sin x :=
id                           └┘         └┘  
src                          └┘          └┘
typ                          └┘         └┘  
doc    └──┘
738  by simp [sin, exp_neg, (neg_div _ _).symm, add_mul]
id            └─┘
src           └─┘
typ           └─┘
739  
740  lemma sin_add : sin (x + y) = sin x * cos y + cos x * sin y :=
id                   └┘          └┘           └┘        
src                  └┘            └┘             └┘      
typ                  └┘          └┘           └┘        
741  by rw [← of_real_inj]; simp [sin, sin_add]
id                                └─┘
src                               └─┘
typ                               └─┘
742  
743  @[simp] lemma cos_zero : cos 0 = 1 := by simp [cos]
id                            └┘                    └─┘
src                           └┘                    └─┘
typ                           └┘                    └─┘
doc    └──┘
744  
745  @[simp] lemma cos_neg : cos (-x) = cos x :=
id                           └┘        └┘  
src                          └┘         └┘
typ                          └┘        └┘  
doc    └──┘
746  by simp [cos, exp_neg]
id            └─┘
src           └─┘
typ           └─┘
747  
748  lemma cos_add : cos (x + y) = cos x * cos y - sin x * sin y :=
id                   └┘          └┘           └┘        
src                  └┘            └┘             └┘      
typ                  └┘          └┘           └┘        
749  by rw ← of_real_inj; simp [cos, cos_add]
id                              └─┘
src                             └─┘
typ                             └─┘
750  
751  lemma sin_sub : sin (x - y) = sin x * cos y - cos x * sin y :=
id                   └┘          └┘           └┘        
src                  └┘            └┘             └┘      
typ                  └┘          └┘           └┘        
752  by simp [sin_add, sin_neg, cos_neg]
753  
754  lemma cos_sub : cos (x - y) = cos x * cos y + sin x * sin y :=
id                   └┘          └┘           └┘        
src                  └┘            └┘             └┘      
typ                  └┘          └┘           └┘        
755  by simp [cos_add, sin_neg, cos_neg]
756  
757  lemma tan_eq_sin_div_cos : tan x = sin x / cos x :=
id                              └┘           └┘  
src                             └┘             └┘
typ                             └┘           └┘  
758  if h : complex.cos x = 0 then by simp [sin, cos, tan, *, complex.tan, div_eq_mul_inv] at *
id                                         └─┘  └─┘  └─┘     └─────────┘
src                                         └─┘  └─┘  └─┘     └─────────┘
typ                                        └─┘  └─┘  └─┘     └─────────┘
759  else
760    by rw [sin, cos, tan, complex.tan, ← of_real_inj, div_eq_mul_inv, mul_re];
761    simp [norm_sq, (div_div_eq_div_mul _ _ _).symm, div_self h]; refl
id           └─────┘                                                └──┘
src          └─────┘                                                └──┘
typ          └─────┘                                                └──┘
doc                                                                 └──┘
762  
763  @[simp] lemma tan_zero : tan 0 = 0 := by simp [tan]
id                            └┘                    └─┘
src                           └┘                    └─┘
typ                           └┘                    └─┘
doc    └──┘
764  
765  @[simp] lemma tan_neg : tan (-x) = -tan x := by simp [tan, neg_div]
id                           └┘         └┘               └─┘
src                          └┘          └┘                └─┘
typ                          └┘         └┘               └─┘
doc    └──┘
766  
767  lemma sin_sq_add_cos_sq : sin x ^ 2 + cos x ^ 2 = 1 :=
id                             └┘            
src                            └┘          
typ                            └┘            
768  of_real_inj.1 $ by simpa using sin_sq_add_cos_sq x
id                                                    
typ                                                   
769  
770  lemma sin_sq_le_one : sin x ^ 2 ≤ 1 :=
id                         └┘  
src                        └┘
typ                        └┘  
771  by rw ← sin_sq_add_cos_sq x; exact le_add_of_nonneg_right' (pow_two_nonneg _)
772  
773  lemma cos_sq_le_one : cos x ^ 2 ≤ 1 :=
id                         └┘  
src                        └┘
typ                        └┘  
774  by rw ← sin_sq_add_cos_sq x; exact le_add_of_nonneg_left' (pow_two_nonneg _)
775  
776  lemma abs_sin_le_one : abs' (sin x) ≤ 1 :=
id                                └┘  
src                               └┘
typ                               └┘  
777  (mul_self_le_mul_self_iff (_root_.abs_nonneg (sin x)) (by exact zero_le_one)).2 $
id                                                 └┘  
src                                                └┘
typ                                                └┘  
778  by rw [← _root_.abs_mul, abs_mul_self, mul_one, ← pow_two];
779     apply sin_sq_le_one
780  
781  lemma abs_cos_le_one : abs' (cos x) ≤ 1 :=
id                                └┘  
src                               └┘
typ                               └┘  
782  (mul_self_le_mul_self_iff (_root_.abs_nonneg (cos x)) (by exact zero_le_one)).2 $
id                                                 └┘  
src                                                └┘
typ                                                └┘  
783  by rw [← _root_.abs_mul, abs_mul_self, mul_one, ← pow_two];
784     apply cos_sq_le_one
785  
786  lemma sin_le_one : sin x ≤ 1 :=
id                      └┘  
src                     └┘
typ                     └┘  
787  (abs_le.1 (abs_sin_le_one _)).2
788  
789  lemma cos_le_one : cos x ≤ 1 :=
id                      └┘  
src                     └┘
typ                     └┘  
790  (abs_le.1 (abs_cos_le_one _)).2
791  
792  lemma neg_one_le_sin : -1 ≤ sin x :=
id                               └┘  
src                              └┘
typ                              └┘  
793  (abs_le.1 (abs_sin_le_one _)).1
794  
795  lemma neg_one_le_cos : -1 ≤ cos x :=
id                               └┘  
src                              └┘
typ                              └┘  
796  (abs_le.1 (abs_cos_le_one _)).1
797  
798  lemma cos_two_mul : cos (2 * x) = 2 * cos x ^ 2 - 1 :=
id                       └┘               └┘  
src                      └┘                └┘
typ                      └┘               └┘  
799  by rw ← of_real_inj; simp [cos_two_mul]
800  
801  lemma sin_two_mul : sin (2 * x) = 2 * sin x * cos x :=
id                       └┘               └┘        
src                      └┘                └┘      
typ                      └┘               └┘        
802  by rw ← of_real_inj; simp [sin_two_mul]
803  
804  lemma cos_square : cos x ^ 2 = 1 / 2 + cos (2 * x) / 2 :=
id                      └┘                         
src                     └┘                  
typ                     └┘                         
805  of_real_inj.1 $ by simpa using cos_square x
id                                             
typ                                            
806  
807  lemma sin_square : sin x ^ 2 = 1 - cos x ^ 2 :=
id                      └┘                
src                     └┘              
typ                     └┘                
808  eq_sub_iff_add_eq.2 $ sin_sq_add_cos_sq _
809  
810  @[simp] lemma sinh_zero : sinh 0 = 0 := by simp [sinh]
id                             └┘                     └──┘
src                            └┘                     └──┘
typ                            └┘                     └──┘
doc    └──┘
811  
812  @[simp] lemma sinh_neg : sinh (-x) = -sinh x :=
id                            └┘          └┘   
src                           └┘           └┘
typ                           └┘          └┘   
doc    └──┘
813  by simp [sinh, exp_neg, (neg_div _ _).symm, add_mul]
id            └──┘
src           └──┘
typ           └──┘
814  
815  lemma sinh_add : sinh (x + y) = sinh x * cosh y + cosh x * sinh y :=
id                    └┘           └┘      └┘      └┘      └┘   
src                   └┘             └┘       └┘       └┘       └┘
typ                   └┘           └┘      └┘      └┘      └┘   
816  by rw ← of_real_inj; simp [sinh_add]
817  
818  @[simp] lemma cosh_zero : cosh 0 = 1 := by simp [cosh]
id                             └┘                     └──┘
src                            └┘                     └──┘
typ                            └┘                     └──┘
doc    └──┘
819  
820  @[simp] lemma cosh_neg : cosh (-x) = cosh x :=
id                            └┘         └┘   
src                           └┘          └┘
typ                           └┘         └┘   
doc    └──┘
821  by simp [cosh, exp_neg]
id            └──┘
src           └──┘
typ           └──┘
822  
823  lemma cosh_add : cosh (x + y) = cosh x * cosh y + sinh x * sinh y :=
id                    └┘           └┘      └┘      └┘      └┘   
src                   └┘             └┘       └┘       └┘       └┘
typ                   └┘           └┘      └┘      └┘      └┘   
824  by rw ← of_real_inj; simp [cosh, cosh_add]
id                              └──┘
src                             └──┘
typ                             └──┘
825  
826  lemma sinh_sub : sinh (x - y) = sinh x * cosh y - cosh x * sinh y :=
id                    └┘           └┘      └┘      └┘      └┘   
src                   └┘             └┘       └┘       └┘       └┘
typ                   └┘           └┘      └┘      └┘      └┘   
827  by simp [sinh_add, sinh_neg, cosh_neg]
828  
829  lemma cosh_sub : cosh (x - y) = cosh x * cosh y - sinh x * sinh y :=
id                    └┘           └┘      └┘      └┘      └┘   
src                   └┘             └┘       └┘       └┘       └┘
typ                   └┘           └┘      └┘      └┘      └┘   
830  by simp [cosh_add, sinh_neg, cosh_neg]
831  
832  lemma tanh_eq_sinh_div_cosh : tanh x = sinh x / cosh x :=
id                                 └┘      └┘      └┘   
src                                └┘       └┘       └┘
typ                                └┘      └┘      └┘   
833  of_real_inj.1 $ by simp [tanh_eq_sinh_div_cosh]
834  
835  @[simp] lemma tanh_zero : tanh 0 = 0 := by simp [tanh]
id                             └┘                     └──┘
src                            └┘                     └──┘
typ                            └┘                     └──┘
doc    └──┘
836  
837  @[simp] lemma tanh_neg : tanh (-x) = -tanh x := by simp [tanh, neg_div]
id                            └┘          └┘                └──┘
src                           └┘           └┘                 └──┘
typ                           └┘          └┘                └──┘
doc    └──┘
838  
839  open is_absolute_value
840  
841  /- TODO make this private and prove ∀ x -/
842  lemma add_one_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) : x + 1 ≤ exp x :=
id                                                              └┘  
src                                                               └┘
typ                                                             └┘  
843  calc x + 1 ≤ lim (⟨(λ n : ℕ, ((exp' x) n).re), is_cau_seq_re (exp' x)⟩ : cau_seq ℝ abs') :
id                                        └┘                                     
src                                          └┘                                      
typ                                       └┘                                     
844    le_lim (cau_seq.le_of_exists ⟨2,
845      λ j hj, show x + (1 : ℝ) ≤ ((range j).sum (λ m, (x ^ m / m.fact : ℂ))).re,
id                                                          └┘        
src                                                                └┘        
typ                                                         └┘        
doc                                                                 └┘ 
846        from have h₁ : (((λ m : ℕ, (x ^ m / m.fact : ℂ)) ∘ nat.succ) 0).re = x, by simp,
id                                          └┘ └┘        └─┘  └─┘         
src                                            └┘ └┘        └─┘  └─┘     
typ                                         └┘ └┘        └─┘  └─┘         
doc                                             └┘ └┘
847        have h₂ : ((x : ℂ) ^ 0 / nat.fact 0).re = 1, by simp,
id                                └──────┘   └┘
src                                └──────┘   └┘
typ                               └──────┘   └┘
doc                                 └──────┘
848        begin
849          rw [← nat.sub_add_cancel hj, sum_range_succ', sum_range_succ',
850            add_re, add_re, h₁, h₂, add_assoc,
851            ← @sum_hom _ _ _ _ _ _ _ complex.re
id                                      └────────┘
src                                     └────────┘
typ                                     └────────┘
852              (is_add_group_hom.to_is_add_monoid_hom _)],
853          refine le_add_of_nonneg_of_le (sum_nonneg (λ m hm, _)) (le_refl _), dsimp [-nat.fact_succ],
id                                                        
typ                                                       
854          rw [← of_real_pow, ← of_real_nat_cast, ← of_real_div, of_real_re],
855          exact div_nonneg (pow_nonneg hx _) (nat.cast_pos.2 (nat.fact_pos _)),
856        end⟩)
st         └─┘
857  ... = exp x : by rw [exp, complex.exp, ← cau_seq_re, lim_re]
id         └─┘ 
src        └─┘
typ        └─┘ 
st                                                              
858  
859  lemma one_le_exp {x : ℝ} (hx : 0 ≤ x) : 1 ≤ exp x :=
id                                             └┘  
src                                             └┘
typ                                            └┘  
860  by linarith [add_one_le_exp_of_nonneg hx]
861  
862  lemma exp_pos (x : ℝ) : 0 < exp x :=
id                              └┘  
src                             └┘
typ                             └┘  
863  (le_total 0 x).elim (lt_of_lt_of_le zero_lt_one ∘ one_le_exp)
id               
typ              
864    (λ h, by rw [← neg_neg x, real.exp_neg];
865      exact inv_pos (lt_of_lt_of_le zero_lt_one (one_le_exp (neg_nonneg.2 h))))
866  
867  @[simp] lemma abs_exp (x : ℝ) : abs' (exp x) = exp x :=
id                                        └┘      └┘  
src                                       └┘       └┘
typ                                       └┘      └┘  
doc    └──┘
868  abs_of_pos (exp_pos _)
869  
870  lemma exp_strict_mono : strict_mono exp :=
id                                       └┘
src                                      └┘
typ                                      └┘
871  λ x y h, by rw [← sub_add_cancel y x, real.exp_add];
id      
typ     
872    exact (lt_mul_iff_one_lt_left (exp_pos _)).2
873      (lt_of_lt_of_le (by linarith) (add_one_le_exp_of_nonneg (by linarith)))
874  
875  lemma exp_lt_exp {x y : ℝ} : exp x < exp y ↔ x < y := exp_strict_mono.lt_iff_lt
id                               └┘                   └──┘  └──┘  
src                              └┘                       └──┘  └──┘  
typ                              └┘                   └──┘  └──┘  
876  
877  lemma exp_le_exp {x y : ℝ} : exp x ≤ exp y ↔ x ≤ y := exp_strict_mono.le_iff_le
id                               └┘     └┘             └──┘  └──┘  
src                              └┘      └┘                └──┘  └──┘  
typ                              └┘     └┘             └──┘  └──┘  
878  
879  lemma exp_injective : function.injective exp := exp_strict_mono.injective
id                                            └┘      └┘  └┘  └┘  └┘
src                                           └┘      └┘  └┘  └┘  └┘
typ                                           └┘      └┘  └┘  └┘  └┘
880  
881  @[simp] lemma exp_eq_one_iff : exp x = 1 ↔ x = 0 :=
id                                  └┘        
src                                 └┘        
typ                                 └┘        
doc    └──┘
882  by rw [← exp_zero, exp_injective.eq_iff]
883  
884  lemma one_lt_exp_iff {x : ℝ} : 1 < exp x ↔ 0 < x :=
id                                     └┘        
src                                    └┘    
typ                                    └┘        
885  by rw [← exp_zero, exp_lt_exp]
886  
887  lemma exp_lt_one_iff {x : ℝ} : exp x < 1 ↔ x < 0 :=
id                                 └┘        
src                                └┘        
typ                                └┘        
888  by rw [← exp_zero, exp_lt_exp]
889  
890  end real
891  
892  namespace complex
893  
894  lemma sum_div_fact_le {α : Type*} [discrete_linear_ordered_field α] (n j : ℕ) (hn : 0 < n) :
id                                      └┘  └──┘  └──┘  └──┘  └──┘                        
src                                     └┘  └──┘  └──┘  └──┘  └──┘             
typ                                     └┘  └──┘  └──┘  └──┘  └──┘                        
895    (sum (filter (λ k, n ≤ k) (range j)) (λ m : ℕ, (1 / m.fact : α))) ≤ n.succ * (n.fact * n)⁻¹ :=
id                                                    └──┘          └─┘        └┘   
src                                                        └──┘            └─┘         └┘
typ                                                   └──┘          └─┘        └┘   
doc                                                         └──┘                        └┘
896  calc (filter (λ k, n ≤ k) (range j)).sum (λ m : ℕ, (1 / m.fact : α))
id                                                              
src                                                  
typ                                                             
897      = (range (j - n)).sum (λ m, 1 / (m + n).fact) :
id                                           └┘
src                                               └┘
typ                                          └┘
doc                                               └┘
898    sum_bij (λ m _, m - n)
id                       
typ                      
899      (λ m hm, mem_range.2 $ (nat.sub_lt_sub_right_iff (by simp at hm; tauto)).2
id          
typ         
900        (by simp at hm; tauto))
901      (λ m hm, by rw nat.sub_add_cancel; simp at *; tauto)
id          
typ         
902      (λ a₁ a₂ ha₁ ha₂ h,
id          └┘ └┘
typ         └┘ └┘
903        by rwa [nat.sub_eq_iff_eq_add, ← nat.sub_add_comm, eq_comm, nat.sub_eq_iff_eq_add, add_right_inj, eq_comm] at h;
904          simp at *; tauto)
905      (λ b hb, ⟨b + n, mem_filter.2 ⟨mem_range.2 $ nat.add_lt_of_lt_sub_right (mem_range.1 hb), nat.le_add_left _ _⟩,
id                   
typ                  
906        by rw nat.add_sub_cancel⟩)
907  ... ≤ (range (j - n)).sum (λ m, (nat.fact n * n.succ ^ m)⁻¹) :
id                                 └──────┘    └───┘   
src                                   └──────┘      └───┘
typ                                └──────┘    └───┘   
doc                                   └──────┘
908    begin
909      refine  sum_le_sum (assume m n, _),
id                                  
typ                                 
910      rw [one_div_eq_inv, inv_le_inv],
911      { rw [← nat.cast_pow, ← nat.cast_mul, nat.cast_le, add_comm],
912        exact nat.fact_mul_pow_le_fact },
st                                        └┘
913      { exact nat.cast_pos.2 (nat.fact_pos _) },
st                                               └┘
914      { exact mul_pos (nat.cast_pos.2 (nat.fact_pos _)) (pow_pos (nat.cast_pos.2 (nat.succ_pos _)) _) },
st                                                                                                       └┘
915    end
st     └─┘
916  ... = (nat.fact n)⁻¹ * (range (j - n)).sum (λ m, n.succ⁻¹ ^ m) :
id          └──────┘                              └───┘     
src         └──────┘                                   └───┘
typ         └──────┘                              └───┘     
doc         └──────┘
917    by simp [mul_inv', mul_sum.symm, sum_mul.symm, -nat.fact_succ, mul_comm, inv_pow']
918  ... = (n.succ - n.succ * n.succ⁻¹ ^ (j - n)) / (n.fact * n) :
id          └───┘   └───┘   └───┘               └───┘   
src          └───┘    └───┘    └───┘                  └───┘
typ         └───┘   └───┘   └───┘               └───┘   
doc                                                   └───┘
919    have h₁ : (n.succ : α) ≠ 1, from @nat.cast_one α _ _ ▸ mt nat.cast_inj.1
id                └───┘                             
src                └───┘
typ               └───┘                             
920          (mt nat.succ_inj (nat.pos_iff_ne_zero.1 hn)),
921    have h₂ : (n.succ : α) ≠ 0, from nat.cast_ne_zero.2 (nat.succ_ne_zero _),
id                └───┘   
src                └───┘
typ               └───┘   
922    have h₃ : (n.fact * n : α) ≠ 0, from mul_ne_zero (nat.cast_ne_zero.2 (nat.pos_iff_ne_zero.1 (nat.fact_pos _)))
id                └───┘      
src                └───┘
typ               └───┘      
doc                └───┘
923      (nat.cast_ne_zero.2 (nat.pos_iff_ne_zero.1 hn)),
924    have h₄ : (n.succ - 1 : α) = n, by simp,
id                └───┘           
src                └───┘
typ               └───┘           
925    by rw [← geom_series_def, geom_sum_inv h₁ h₂, eq_div_iff_mul_eq _ _ h₃, mul_comm _ (n.fact * n : α),
id                                                                                         └────┘      
src                                                                                        └────┘
typ                                                                                        └────┘      
doc                                                                                        └────┘
926        ← mul_assoc (n.fact⁻¹ : α), ← mul_inv', h₄, ← mul_assoc (n.fact * n : α),
id                      └────┘                                     └────┘      
src                     └────┘                                      └────┘
typ                     └────┘                                     └────┘      
doc                     └────┘                                      └────┘
927        mul_comm (n : α) n.fact, mul_inv_cancel h₃];
id                         └────┘
src                         └────┘
typ                        └────┘
doc                         └────┘
928      simp [mul_add, add_mul, mul_assoc, mul_comm]
929  ... ≤ n.succ / (n.fact * n) :
id         └───┘    └───┘   
src         └───┘     └───┘
typ        └───┘    └───┘   
doc                   └───┘
930    begin
931      refine (div_le_div_right (mul_pos _ _)).2 _,
932      exact nat.cast_pos.2 (nat.fact_pos _),
933      exact nat.cast_pos.2 hn,
934      exact sub_le_self _ (mul_nonneg (nat.cast_nonneg _) (pow_nonneg (inv_nonneg.2 (nat.cast_nonneg _)) _))
935    end
st     └─┘
936  
937  lemma exp_bound {x : ℂ} (hx : abs x ≤ 1) {n : ℕ} (hn : 0 < n) :
id                                └┘                         
src                               └┘              
typ                               └┘                         
938    abs (exp x - (range n).sum (λ m, x ^ m / m.fact)) ≤ abs x ^ n * (n.succ * (n.fact * n)⁻¹) :=
id      └┘                                └┘ └┘     └┘          └─┘    └┘ └┘   
src     └┘                                      └┘ └┘     └┘             └─┘     └┘ └┘
typ     └┘                                └┘ └┘     └┘          └─┘    └┘ └┘   
doc                                              └┘ └┘                             └┘ └┘
939  begin
940    rw [← lim_const ((range n).sum _), exp, sub_eq_add_neg, ← lim_neg, lim_add, ← lim_abs],
941    refine lim_le (cau_seq.le_of_exists ⟨n, λ j hj, _⟩),
id                                               └┘
typ                                              └┘
942    show abs ((range j).sum (λ m, x ^ m / m.fact) - (range n).sum (λ m, x ^ m / m.fact))
id                                                                    
typ                                                                   
943      ≤ abs x ^ n * (n.succ * (n.fact * n)⁻¹),
id         └─┘         └────┘    └────┘   
src        └─┘          └────┘    └────┘
typ        └─┘         └────┘    └────┘   
doc                               └────┘
944    rw sum_range_sub_sum_range hj,
id                                └┘
typ                               └┘
945    exact calc abs (((range j).filter (λ k, n ≤ k)).sum (λ m : ℕ, (x ^ m / m.fact : ℂ)))
id                                          
typ                                         
946        = abs (((range j).filter (λ k, n ≤ k)).sum (λ m : ℕ, (x ^ n * (x ^ (m - n) / m.fact) : ℂ))) :
id                                                                              
typ                                                                             
947      congr_arg abs (sum_congr rfl (λ m hm, by rw [← mul_div_assoc, ← pow_add, nat.add_sub_cancel']; simp at hm; tauto))
id                                       
typ                                      
948    ... ≤ sum (filter (λ k, n ≤ k) (range j)) (λ m, abs (x ^ n * (_ / m.fact))) : abv_sum_le_sum_abv _ _
id                                                 
typ                                                
949    ... ≤ sum (filter (λ k, n ≤ k) (range j)) (λ m, abs x ^ n * (1 / m.fact)) :
id                                                 
typ                                                
950      begin
951        refine sum_le_sum (λ m hm, _),
id                              
typ                             
952        rw [abs_mul, abv_pow abs, abs_div, abs_cast_nat],
id                              └─┘
src                             └─┘
typ                             └─┘
953        refine mul_le_mul_of_nonneg_left ((div_le_div_right _).2 _) _,
954        exact nat.cast_pos.2 (nat.fact_pos _),
955        rw abv_pow abs,
id                    └─┘
src                   └─┘
typ                   └─┘
956        exact (pow_le_one _ (abs_nonneg _) hx),
957        exact pow_nonneg (abs_nonneg _) _
958      end
st       └─┘
959    ... = abs x ^ n * (((range j).filter (λ k, n ≤ k)).sum (λ m : ℕ, (1 / m.fact : ℝ))) :
id                                             
typ                                            
960      by simp [abs_mul, abv_pow abs, abs_div, mul_sum.symm]
id                                 └─┘
src                                └─┘
typ                                └─┘
961    ... ≤ abs x ^ n * (n.succ * (n.fact * n)⁻¹) :
id                        └────┘    └────┘
src                       └────┘    └────┘
typ                       └────┘    └────┘
doc                                 └────┘
962      mul_le_mul_of_nonneg_left (sum_div_fact_le _ _ hn) (pow_nonneg (abs_nonneg _) _)
963  end
st   └─┘
964  
965  lemma abs_exp_sub_one_le {x : ℂ} (hx : abs x ≤ 1) :
id                                         └┘  
src                                        └┘
typ                                        └┘  
966    abs (exp x - 1) ≤ 2 * abs x :=
id      └┘                 └┘  
src     └┘                  └┘
typ     └┘                 └┘  
967  calc abs (exp x - 1) = abs (exp x - (range 1).sum (λ m, x ^ m / m.fact)) :
id                       └┘    └┘                              └──┘
src                       └┘    └┘                                   └──┘
typ                      └┘    └┘                              └──┘
doc                                                                    └──┘
968    by simp [sum_range_succ]
969  ... ≤ abs x ^ 1 * ((nat.succ 1) * (nat.fact 1 * (1 : ℕ))⁻¹) :
id         └─┘          └──────┘       └──────┘          
src        └─┘           └──────┘       └──────┘          
typ        └─┘          └──────┘       └──────┘          
doc                                     └──────┘
970    exp_bound hx dec_trivial
971  ... = 2 * abs x : by simp [two_mul, mul_two, mul_add, mul_comm]
id             └─┘ 
src            └─┘
typ            └─┘ 
972  
973  lemma abs_exp_sub_one_sub_id_le {x : ℂ} (hx : abs x ≤ 1) :
id                                                └┘  
src                                               └┘
typ                                               └┘  
974    abs (exp x - 1 - x) ≤ (abs x)^2 :=
id      └┘                 └┘  
src     └┘                   └┘
typ     └┘                 └┘  
975  calc abs (exp x - 1 - x) = abs (exp x - (range 2).sum (λ m, x ^ m / m.fact)) :
id                             └┘                                  └──┘
src                              └┘                                       └──┘
typ                            └┘                                  └──┘
doc                                                                        └──┘
976    by simp [sum_range_succ]
977  ... ≤ (abs x)^2 * (nat.succ 2 * (nat.fact 2 * (2 : ℕ))⁻¹) :
id          └─┘        └──────┘      └──────┘          
src         └─┘         └──────┘      └──────┘          
typ         └─┘        └──────┘      └──────┘          
doc                                   └──────┘
978    exp_bound hx dec_trivial
979  ... ≤ (abs x)^2 * 1 :
id          └─┘ 
src         └─┘
typ         └─┘ 
980    mul_le_mul_of_nonneg_left (by norm_num) (pow_two_nonneg (abs x))
id                                                              └─┘ 
src                                                             └─┘
typ                                                             └─┘ 
981  ... = (abs x)^2 :
id          └─┘ 
src         └─┘
typ         └─┘ 
982    by rw [mul_one]
st                   
983  
984  end complex
985  
986  namespace real
987  
988  open complex finset
989  
990  lemma cos_bound {x : ℝ} (hx : abs' x ≤ 1) : abs' (cos x - (1 - x ^ 2 / 2)) ≤ abs' x ^ 4 * (5 / 96) :=
id                                                   └┘                            
src                                                   └┘
typ                                                  └┘                            
991  calc abs' (cos x - (1 - x ^ 2 / 2)) = abs (complex.cos x - (1 - x ^ 2 / 2)) :
id                                       └┘    └┘  └┘  └┘         
src                                        └┘    └┘  └┘  └┘
typ                                      └┘    └┘  └┘  └┘         
992    by rw ← abs_of_real; simp [of_real_bit0, of_real_one, of_real_inv]
993  ... = abs ((complex.exp (x * I) + complex.exp (-x * I) - (2 - x ^ 2)) / 2) :
id         └─┘   └─────────┘         └─────────┘               
src        └─┘   └─────────┘          └─────────┘       
typ        └─┘   └─────────┘         └─────────┘               
994    by simp [complex.cos, sub_div, add_div, neg_div, div_self (@two_ne_zero' ℂ _ _ _)]
id              └─────────┘
src             └─────────┘
typ             └─────────┘
995  ... = abs (((complex.exp (x * I) - (range 4).sum (λ m, (x * I) ^ m / m.fact)) +
id         └─┘    └─────────┘                                       └───┘
src        └─┘    └─────────┘                                            └───┘
typ        └─┘    └─────────┘                                       └───┘
doc                                                                        └───┘
996      ((complex.exp (-x * I) - (range 4).sum (λ m, (-x * I) ^ m / m.fact)))) / 2) :
id         └─────────┘                                         └───┘
src        └─────────┘                                              └───┘
typ        └─────────┘                                         └───┘
doc                                                                   └───┘
997    congr_arg abs (congr_arg (λ x : ℂ, x / 2) begin
id               └─┘                     
src              └─┘                   
typ              └─┘                     
998      simp only [sum_range_succ],
999      simp [pow_succ],
1000      apply complex.ext; simp [div_eq_mul_inv, norm_sq]; ring
id                                                └─────┘
src                                               └─────┘
typ                                               └─────┘
1001    end)
st     └─┘
1002  ... ≤ abs ((complex.exp (x * I) - (range 4).sum (λ m, (x * I) ^ m / m.fact)) / 2) +
id         └─┘   └─────────┘                                       └───┘
src        └─┘   └─────────┘                                            └───┘
typ        └─┘   └─────────┘                                       └───┘
doc                                                                       └───┘
1003      abs ((complex.exp (-x * I) - (range 4).sum (λ m, (-x * I) ^ m / m.fact)) / 2) :
id       └─┘   └─────────┘                                         └───┘
src      └─┘   └─────────┘                                              └───┘
typ      └─┘   └─────────┘                                         └───┘
doc                                                                       └───┘
1004    by rw add_div; exact abs_add _ _
1005  ... = (abs ((complex.exp (x * I) - (range 4).sum (λ m, (x * I) ^ m / m.fact))) / 2 +
id          └─┘   └─────────┘                                       └───┘
src         └─┘   └─────────┘                                            └───┘
typ         └─┘   └─────────┘                                       └───┘
doc                                                                        └───┘
1006      abs ((complex.exp (-x * I) - (range 4).sum (λ m, (-x * I) ^ m / m.fact))) / 2) :
id       └─┘   └─────────┘                                         └───┘
src      └─┘   └─────────┘                                              └───┘
typ      └─┘   └─────────┘                                         └───┘
doc                                                                       └───┘
1007    by simp [complex.abs_div]
1008  ... ≤ ((complex.abs (x * I) ^ 4 * (nat.succ 4 * (nat.fact 4 * (4 : ℕ))⁻¹)) / 2 +
id           └─────────┘              └──────┘      └──────┘          
src          └─────────┘               └──────┘      └──────┘          
typ          └─────────┘              └──────┘      └──────┘          
doc                                                   └──────┘
1009      (complex.abs (-x * I) ^ 4 * (nat.succ 4 * (nat.fact 4 * (4 : ℕ))⁻¹)) / 2)  :
id        └─────────┘               └──────┘      └──────┘          
src       └─────────┘                └──────┘      └──────┘          
typ       └─────────┘               └──────┘      └──────┘          
doc                                                 └──────┘
1010    add_le_add ((div_le_div_right (by norm_num)).2 (exp_bound (by simpa) dec_trivial))
1011               ((div_le_div_right (by norm_num)).2 (exp_bound (by simpa) dec_trivial))
1012  ... ≤ abs' x ^ 4 * (5 / 96) : by norm_num; simp [mul_assoc, mul_comm, mul_left_comm, mul_div_assoc]
id              
typ             
1013  
1014  lemma sin_bound {x : ℝ} (hx : abs' x ≤ 1) : abs' (sin x - (x - x ^ 3 / 6)) ≤ abs' x ^ 4 * (5 / 96) :=
id                                                    └┘                           
src                                                   └┘
typ                                                   └┘                           
1015  calc abs' (sin x - (x - x ^ 3 / 6)) = abs (complex.sin x - (x - x ^ 3 / 6)) :
id                                      └┘    └┘  └┘  └┘        
src                                        └┘    └┘  └┘  └┘
typ                                     └┘    └┘  └┘  └┘        
1016    by rw ← abs_of_real; simp [of_real_bit0, of_real_one, of_real_inv]
1017  ... = abs (((complex.exp (-x * I) - complex.exp (x * I)) * I - (2 * x - x ^ 3 / 3)) / 2) :
id         └─┘    └─────────┘          └─────────┘                     
src        └─┘    └─────────┘           └─────────┘           
typ        └─┘    └─────────┘          └─────────┘                     
1018    by simp [complex.sin, sub_div, add_div, neg_div, mul_div_cancel_left _ (@two_ne_zero' ℂ _ _ _),
id              └─────────┘
src             └─────────┘
typ             └─────────┘
1019      div_div_eq_div_mul, show (3 : ℂ) * 2 = 6, by norm_num]
1020  ... = abs ((((complex.exp (-x * I) - (range 4).sum (λ m, (-x * I) ^ m / m.fact)) -
id         └─┘     └─────────┘                                         └───┘
src        └─┘     └─────────┘                                              └───┘
typ        └─┘     └─────────┘                                         └───┘
doc                                                                           └───┘
1021      (complex.exp (x * I) - (range 4).sum (λ m, (x * I) ^ m / m.fact))) * I) / 2) :
id        └─────────┘                                       └───┘      
src       └─────────┘                                            └───┘      
typ       └─────────┘                                       └───┘      
doc                                                                └───┘
1022    congr_arg abs (congr_arg (λ x : ℂ, x / 2) begin
id               └─┘                     
src              └─┘                   
typ              └─┘                     
1023      simp only [sum_range_succ],
1024      simp [pow_succ],
1025      apply complex.ext; simp [div_eq_mul_inv, norm_sq]; ring
id                                                └─────┘
src                                               └─────┘
typ                                               └─────┘
1026    end)
st     └─┘
1027  ... ≤ abs ((complex.exp (-x * I) - (range 4).sum (λ m, (-x * I) ^ m / m.fact)) * I / 2) +
id         └─┘   └─────────┘                                         └───┘     
src        └─┘   └─────────┘                                              └───┘     
typ        └─┘   └─────────┘                                         └───┘     
doc                                                                         └───┘
1028      abs (-((complex.exp (x * I) - (range 4).sum (λ m, (x * I) ^ m / m.fact)) * I) / 2) :
id       └─┘     └─────────┘                                       └───┘     
src      └─┘     └─────────┘                                            └───┘     
typ      └─┘     └─────────┘                                       └───┘     
doc                                                                       └───┘
1029    by rw [sub_mul, sub_eq_add_neg, add_div]; exact abs_add _ _
1030  ... = (abs ((complex.exp (x * I) - (range 4).sum (λ m, (x * I) ^ m / m.fact))) / 2 +
id          └─┘   └─────────┘                                       └───┘
src         └─┘   └─────────┘                                            └───┘
typ         └─┘   └─────────┘                                       └───┘
doc                                                                        └───┘
1031      abs ((complex.exp (-x * I) - (range 4).sum (λ m, (-x * I) ^ m / m.fact))) / 2) :
id       └─┘   └─────────┘                                         └───┘
src      └─┘   └─────────┘                                              └───┘
typ      └─┘   └─────────┘                                         └───┘
doc                                                                       └───┘
1032    by simp [complex.abs_div, complex.abs_mul]
1033  ... ≤ ((complex.abs (x * I) ^ 4 * (nat.succ 4 * (nat.fact 4 * (4 : ℕ))⁻¹)) / 2 +
id           └─────────┘              └──────┘      └──────┘          
src          └─────────┘               └──────┘      └──────┘          
typ          └─────────┘              └──────┘      └──────┘          
doc                                                   └──────┘
1034      (complex.abs (-x * I) ^ 4 * (nat.succ 4 * (nat.fact 4 * (4 : ℕ))⁻¹)) / 2) :
id        └─────────┘               └──────┘      └──────┘          
src       └─────────┘                └──────┘      └──────┘          
typ       └─────────┘               └──────┘      └──────┘          
doc                                                 └──────┘
1035    add_le_add ((div_le_div_right (by norm_num)).2 (exp_bound (by simpa) dec_trivial))
1036               ((div_le_div_right (by norm_num)).2 (exp_bound (by simpa) dec_trivial))
1037  ... ≤ abs' x ^ 4 * (5 / 96) : by norm_num; simp [mul_assoc, mul_comm, mul_left_comm, mul_div_assoc]
id              
typ             
1038  
1039  lemma cos_pos_of_le_one {x : ℝ} (hx : abs' x ≤ 1) : 0 < cos x :=
id                                                         └┘  
src                                                         └┘
typ                                                        └┘  
1040  calc 0 < (1 - x ^ 2 / 2) - abs' x ^ 4 * (5 / 96) :
id                                  
typ                                 
1041    sub_pos.2 $ lt_sub_iff_add_lt.2
1042      (calc abs' x ^ 4 * (5 / 96) + x ^ 2 / 2
id                                    
typ                                   
1043            ≤ 1 * (5 / 96) + 1 / 2 :
1044          add_le_add
1045            (mul_le_mul_of_nonneg_right (pow_le_one _ (abs_nonneg _) hx) (by norm_num))
1046            ((div_le_div_right (by norm_num)).2 (by rw [pow_two, ← abs_mul_self, _root_.abs_mul];
1047              exact mul_le_one hx (abs_nonneg _) hx))
1048        ... < 1 : by norm_num)
1049  ... ≤ cos x : sub_le.1 (abs_sub_le_iff.1 (cos_bound hx)).2
id         └─┘ 
src        └─┘
typ        └─┘ 
1050  
1051  lemma sin_pos_of_pos_of_le_one {x : ℝ} (hx0 : 0 < x) (hx : x ≤ 1) : 0 < sin x :=
id                                                                        └┘  
src                                                                         └┘
typ                                                                       └┘  
1052  calc 0 < x - x ^ 3 / 6 - abs' x ^ 4 * (5 / 96) :
id                               
typ                              
1053    sub_pos.2 $ lt_sub_iff_add_lt.2
1054      (calc abs' x ^ 4 * (5 / 96) + x ^ 3 / 6
id                                    
typ                                   
1055          ≤ x * (5 / 96) + x / 6 :
id                            
typ                           
1056        add_le_add
1057          (mul_le_mul_of_nonneg_right
1058            (calc abs' x ^ 4 ≤ abs' x ^ 1 : pow_le_pow_of_le_one (abs_nonneg _)
id                                    
typ                                   
1059                  (by rwa _root_.abs_of_nonneg (le_of_lt hx0))
1060                  dec_trivial
1061              ... = x : by simp [_root_.abs_of_nonneg (le_of_lt (hx0))]) (by norm_num))
id                     
typ                    
1062          ((div_le_div_right (by norm_num)).2
1063            (calc x ^ 3 ≤ x ^ 1 : pow_le_pow_of_le_one (le_of_lt hx0) hx dec_trivial
id                          
typ                         
1064              ... = x : pow_one _))
id                     
typ                    
1065      ... < x : by linarith)
id             
typ            
1066  ... ≤ sin x : sub_le.1 (abs_sub_le_iff.1 (sin_bound
id         └─┘ 
src        └─┘
typ        └─┘ 
1067      (by rwa [_root_.abs_of_nonneg (le_of_lt hx0)]))).2
1068  
1069  lemma sin_pos_of_pos_of_le_two {x : ℝ} (hx0 : 0 < x) (hx : x ≤ 2) : 0 < sin x :=
id                                                                        └┘  
src                                                                         └┘
typ                                                                       └┘  
1070  have x / 2 ≤ 1, from div_le_of_le_mul (by norm_num) (by simpa),
id        
typ       
1071  calc 0 < 2 * sin (x / 2) * cos (x / 2) :
id                └─┘          └─┘  
src               └─┘           └─┘
typ               └─┘          └─┘  
1072    mul_pos (mul_pos (by norm_num) (sin_pos_of_pos_of_le_one (half_pos hx0) this))
1073      (cos_pos_of_le_one (by rwa [_root_.abs_of_nonneg (le_of_lt (half_pos hx0))]))
1074  ... = sin x : by rw [← sin_two_mul, two_mul, add_halves]
id         └─┘ 
src        └─┘
typ        └─┘ 
st                                                          
1075  
1076  lemma cos_one_le : cos 1 ≤ 2 / 3 :=
id                      └┘
src                     └┘
typ                     └┘
1077  calc cos 1 ≤ abs' (1 : ℝ) ^ 4 * (5 / 96) + (1 - 1 ^ 2 / 2) :
id                         
src                        
typ                        
1078    sub_le_iff_le_add.1 (abs_sub_le_iff.1 (cos_bound (by simp))).1
1079  ... ≤ 2 / 3 : by norm_num
1080  
1081  lemma cos_one_pos : 0 < cos 1 := cos_pos_of_le_one (by simp)
id                           └┘
src                          └┘
typ                          └┘
1082  
1083  lemma cos_two_neg : cos 2 < 0 :=
id                       └┘
src                      └┘
typ                      └┘
1084  calc cos 2 = cos (2 * 1) : congr_arg cos (mul_one _).symm
id                └┘                      └┘
src               └┘                      └┘
typ               └┘                      └┘
1085  ... = _ : real.cos_two_mul 1
1086  ... ≤ 2 * (2 / 3) ^ 2 - 1 :
1087    sub_le_sub_right (mul_le_mul_of_nonneg_left
1088      (by rw [pow_two, pow_two]; exact
1089        mul_self_le_mul_self (le_of_lt cos_one_pos)
1090          cos_one_le)
1091      (by norm_num)) _
1092  ... < 0 : by norm_num
1093  
1094  end real
1095  
1096  namespace complex
1097  
1098  lemma abs_cos_add_sin_mul_I (x : ℝ) : abs (cos x + sin x * I) = 1 :=
id                                        └┘    └┘          
src                                       └┘    └┘            
typ                                       └┘    └┘          
1099  have _ := real.sin_sq_add_cos_sq x,
id                                    
typ                                   
1100  by simp [abs, norm_sq, pow_two, *, sin_of_real_re, cos_of_real_re, mul_re] at *
id            └─┘  └─────┘
src           └─┘  └─────┘
typ           └─┘  └─────┘
1101  
1102  lemma abs_exp_eq_iff_re_eq {x y : ℂ} : abs (exp x) = abs (exp y) ↔ x.re = y.re :=
id                                         └┘    └┘         └┘       └─┘   └┘
src                                        └┘    └┘          └┘        └─┘    └┘
typ                                        └┘    └┘         └┘       └─┘   └┘
1103  by rw [exp_eq_exp_re_mul_sin_add_cos, exp_eq_exp_re_mul_sin_add_cos y,
1104      abs_mul, abs_mul, abs_cos_add_sin_mul_I, abs_cos_add_sin_mul_I,
1105      ← of_real_exp, ← of_real_exp, abs_of_nonneg (le_of_lt (real.exp_pos _)),
1106      abs_of_nonneg (le_of_lt (real.exp_pos _)), mul_one, mul_one];
1107    exact ⟨λ h, real.exp_injective h, congr_arg _⟩
id                 └────────────────┘
src                └────────────────┘
typ                └────────────────┘
1108  
1109  @[simp] lemma abs_exp_of_real (x : ℝ) : abs (exp x) = real.exp x :=
id                                          └┘    └┘       └┘   
src                                         └┘    └┘        └┘  
typ                                         └┘    └┘       └┘   
doc    └──┘
1110  by rw [← of_real_exp]; exact abs_of_nonneg (le_of_lt (real.exp_pos _))
1111  
1112  end complex